emacs-elpa-diffs
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[nongnu] elpa/proof-general bf43cfb39a: Add Coq tactic "native_compute"


From: ELPA Syncer
Subject: [nongnu] elpa/proof-general bf43cfb39a: Add Coq tactic "native_compute" (#680)
Date: Wed, 8 Mar 2023 18:01:27 -0500 (EST)

branch: elpa/proof-general
commit bf43cfb39a6deaea56a96d8e889e91319ec4dbc1
Author: Shengyi Wang <txyyss@gmail.com>
Commit: GitHub <noreply@github.com>

    Add Coq tactic "native_compute" (#680)
---
 coq/coq-syntax.el | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 68c10abd19..012081f0f3 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -246,6 +246,7 @@ so for the following reasons:
      ("move after" "mov" "move # after #" t "move")
      ("multimatch with" "mm" "multimatch # with\n| # => #\nend")
      ("multi_match! with" "multi_m" "multi_match! # with\n| # => #\nend")
+     ("native_compute" "nac" "native_compute" t "native_compute")
      ("nia" nil "nia" t "nia")
      ("now_show" nil "now_show" t "now_show")
      ("nra" nil "nra" t "nra")
@@ -506,7 +507,7 @@ so for the following reasons:
     ("Ltac2" "lt2m" "Ltac2 mutable # := #." t "Ltac2 mutable")
     ("Ltac2" "lt2r" "Ltac2 rec # := #." t "Ltac2 rec")
     ("Ltac2" "lt2s" "Ltac2 Set # := #." t "Ltac2 Set")
-    ("Ltac2" "lt2" "Ltac2 # := #." t "Ltac2") 
+    ("Ltac2" "lt2" "Ltac2 # := #." t "Ltac2")
     ("Local Ltac" nil "Local Ltac # := #." t "Local\\s-+Ltac")
     ("Ltac" "ltac" "Ltac # := #." t "Ltac")
     ("Module :=" "mo" "Module # : # := #." t ) ; careful
@@ -1130,7 +1131,7 @@ different."
   "Value for `proof-script-definition-end-regexp'."
   :type 'regexp
   :group 'coq)
-  
+
 (defcustom coq-omit-proof-admit-command "Admitted."
   "Value for `proof-script-proof-admit-command'."
   :type 'string



reply via email to

[Prev in Thread] Current Thread [Next in Thread]