[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
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [nongnu] elpa/proof-general bf43cfb39a: Add Coq tactic "native_compute" (#680),
ELPA Syncer <=