From 236748ccf8ee0b305bf7892138db55425ccc1b36 Mon Sep 17 00:00:00 2001
From: Matus Goljer <matus.goljer@gmail.com>
Date: Sat, 29 Jun 2024 20:15:00 +0200
Subject: [PATCH] feat(coq): add basic config for Coq

Fixes #1007
---
 smartparens-config.el |  1 +
 smartparens-coq.el    | 60 +++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 61 insertions(+)
 create mode 100644 smartparens-coq.el

diff --git a/smartparens-config.el b/smartparens-config.el
index 7d328b42..80ab8202 100644
--- a/smartparens-config.el
+++ b/smartparens-config.el
@@ -131,6 +131,7 @@ ID, ACTION, CONTEXT."
 (eval-after-load 'cc-mode                  '(require 'smartparens-c))
 (--each '(clojure-mode clojure-ts-mode)
   (eval-after-load it                      '(require 'smartparens-clojure)))
+(eval-after-load 'coq-mode                 '(require 'smartparens-coq))
 (eval-after-load 'crystal-mode             '(require 'smartparens-crystal))
 (eval-after-load 'elixir-mode              '(require 'smartparens-elixir))
 (eval-after-load 'elixir-ts-mode           '(require 'smartparens-elixir))
diff --git a/smartparens-coq.el b/smartparens-coq.el
new file mode 100644
index 00000000..c84a6cfc
--- /dev/null
+++ b/smartparens-coq.el
@@ -0,0 +1,60 @@
+;;; smartparens-coq.el --- Additional configuration for Coq proof assistant -*- lexical-binding: t; -*-
+
+;; Copyright (C) 2024 Matus Goljer
+
+;; Author: Matus Goljer <matus.goljer@gmail.com>
+;; Maintainer: Matus Goljer <matus.goljer@gmail.com>
+;; Created: 29 June 2024
+;; Keywords: smartparens, coq
+;; URL: https://github.com/Fuco1/smartparens
+
+;; This file is not part of GNU Emacs.
+
+;;; License:
+
+;; This file is part of Smartparens.
+
+;; Smartparens is free software; you can redistribute it and/or modify
+;; it under the terms of the GNU General Public License as published by
+;; the Free Software Foundation, either version 3 of the License, or
+;; (at your option) any later version.
+
+;; Smartparens is distributed in the hope that it will be useful,
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;; GNU General Public License for more details.
+
+;; You should have received a copy of the GNU General Public License
+;; along with Smartparens.  If not, see <http://www.gnu.org/licenses/>.
+
+;;; Commentary:
+
+;; This file provides some additional configuration for Coq proof
+;; assistant.  To use it, simply add:
+;;
+;; (require 'smartparens-coq)
+;;
+;; into your configuration.  You can use this in conjunction with the
+;; default config or your own configuration.
+;;
+;; If you have good ideas about what should be added please file an
+;; issue on the github tracker.
+;;
+;; For more info, see github readme at
+;; https://github.com/Fuco1/smartparens
+
+;;; Code:
+
+(require 'smartparens)
+
+(sp-with-modes '(coq-mode)
+  ;; Disable ' because it is used in pattern-matching
+  (sp-local-pair "'" nil :actions nil)
+  ;; Disable ` because it is used in polymorphic variants
+  (sp-local-pair "`" nil :actions nil)
+  (sp-local-pair "(*" "*)"
+                 :post-handlers '(("| " "SPC")
+                                  (" | " "*"))))
+
+(provide 'smartparens-coq)
+;;; smartparens-coq.el ends here