[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general cc2941fbf2 1/2: coq-syntax.el: Fix STATECH b
From: |
ELPA Syncer |
Subject: |
[nongnu] elpa/proof-general cc2941fbf2 1/2: coq-syntax.el: Fix STATECH booleans (t => the command is not state-preserving) (#692) |
Date: |
Sun, 26 Mar 2023 20:02:53 -0400 (EDT) |
branch: elpa/proof-general
commit cc2941fbf27c82d02c66cd7c2e7333315c41a70b
Author: Erik Martin-Dorel <erik@martin-dorel.org>
Commit: GitHub <noreply@github.com>
coq-syntax.el: Fix STATECH booleans (t => the command is not
state-preserving) (#692)
---
coq/coq-syntax.el | 45 ++++++++++++++++++++++-----------------------
1 file changed, 22 insertions(+), 23 deletions(-)
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 012081f0f3..e485449b91 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -559,7 +559,7 @@ so for the following reasons:
("Theorem" "th" "Theorem # : #.\n#\nQed." t "Theorem")
("Program Theorem" "pth" "Program Theorem # : #.\nProof.\n#\nQed." t
"Program\\s-+Theorem")
("Obligation" "obl" "Obligation #.\n#\nQed." t "Obligation")
- ("Obligations" "obls" "Obligations #.\n#\nQed." nil "Obligations")
+ ("Obligations" "obls" "Obligations #.\n#\nQed." t "Obligations")
("Next Obligation" "nobl" "Next Obligation.\n#\nQed." t "Next Obligation")
)
"Coq goal starters keywords information list. See `coq-syntax-db' for
syntax."
@@ -574,7 +574,7 @@ so for the following reasons:
("About" nil "About #." nil "About")
("Check" nil "Check" nil "Check")
("Compute" nil "Compute" nil "Compute")
- ("Fail" nil "Fail" nil "fail")
+ ("Fail" nil "Fail" nil "Fail")
("Inspect" nil "Inspect #." nil "Inspect")
("Locate File" nil "Locate File \"#\"." nil "Locate\\s-+File")
("Locate Library" nil "Locate Library #." nil "Locate\\s-+Library")
@@ -604,40 +604,40 @@ They deserve a separate menu for sending them to Coq
without insertion.")
("Add Abstract Ring" nil "Add Abstract Ring #." t
"Add\\s-+Abstract\\s-+Ring")
("Add Abstract Semi Ring" nil "Add Abstract Semi Ring #." t
"Add\\s-+Abstract\\s-+Semi\\s-+Ring")
("Add Field" nil "Add Field #." t "Add\\s-+Field")
- ("Add LoadPath" nil "Add LoadPath #." nil "Add\\s-+LoadPath")
- ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path")
+ ("Add LoadPath" nil "Add LoadPath #." t "Add\\s-+LoadPath")
+ ("Add ML Path" nil "Add ML Path #." t "Add\\s-+ML\\s-+Path")
("Add Printing" nil "Add Printing #." t "Add\\s-+Printing")
("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If")
("Add Printing Let" nil "Add Printing Let #." t "Add\\s-+Printing\\s-+Let")
- ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil
"Add\\s-+Rec\\s-+LoadPath")
- ("Add Rec ML Path" nil "Add Rec ML Path #." nil
"Add\\s-+Rec\\s-+ML\\s-+Path")
+ ("Add Rec LoadPath" nil "Add Rec LoadPath #." t "Add\\s-+Rec\\s-+LoadPath")
+ ("Add Rec ML Path" nil "Add Rec ML Path #." t
"Add\\s-+Rec\\s-+ML\\s-+Path")
("Add Ring" nil "Add Ring #." t "Add\\s-+Ring")
("Add Semi Ring" nil "Add Semi Ring #." t "Add\\s-+Semi\\s-+Ring")
("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid")
- ("Admit Obligations" "oblsadmit" "Admit Obligations." nil
"Admit\\s-+Obligations")
+ ("Admit Obligations" "oblsadmit" "Admit Obligations." t
"Admit\\s-+Obligations")
("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t
"Arguments\\s-+Scope")
("Local Arguments" nil "Local Arguments @{id} : @{rule}" t
"Local\\s-+Arguments")
("Arguments" "args" "Arguments @{id} : @{rule}" t "Arguments")
("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t
"Bind\\s-+Scope")
("Canonical" nil "Canonical #." t "Canonical")
- ("Cd" nil "Cd #." nil "Cd")
+ ("Cd" nil "Cd #." t "Cd")
("Local Close Scope" "lclsc" "Local Close Scope #" t
"Local\\s-+Close\\s-+Scope")
("Close Scope" "clsc" "Close Scope #" t "Close\\s-+Scope")
("Comments" nil "Comments #." nil "Comments")
- ("Declare" nil "Declare #." nil "Declare")
+ ("Declare" nil "Declare #." t "Declare")
("Delimit Scope" "delsc" "Delimit Scope @{scope} with @{id}." t
"Delimit\\s-+Scope" )
("Eval" nil "Eval #." nil "Eval")
("Export" nil "Export #." t "Export")
- ("Extract Constant" "extrc" "Extract Constant @{id} => \"@{id}\"." nil
"Extract\\s-+Constant")
- ("Extract Inlined Constant" "extric" "Extract Inlined Constant @{id} =>
\"@{id}\"." nil "Extract\\s-+Inlined\\s-+Constant")
- ("Extract Inductive" "extri" "Extract Inductive @{id} => \"@{id}\"
[\"@{id}\" \"@{id...}\"]." nil "Extract")
+ ("Extract Constant" "extrc" "Extract Constant @{id} => \"@{id}\"." t
"Extract\\s-+Constant")
+ ("Extract Inlined Constant" "extric" "Extract Inlined Constant @{id} =>
\"@{id}\"." t "Extract\\s-+Inlined\\s-+Constant")
+ ("Extract Inductive" "extri" "Extract Inductive @{id} => \"@{id}\"
[\"@{id}\" \"@{id...}\"]." t "Extract")
("Extraction (in a file)" "extrf" "Extraction \"@{file}\" @{id}." nil)
("Extraction Inline" nil "Extraction Inline #." t "Extraction\\s-+Inline")
("Extraction NoInline" nil "Extraction NoInline #." t
"Extraction\\s-+NoInline")
("Extraction Language" "extrlang" "Extraction Language #." t
"Extraction\\s-+Language")
("Extraction Library" "extrl" "Extraction Library @{id}." nil
"Extraction\\s-+Library")
("Extraction" "extr" "Extraction @{id}." nil "Extraction")
- ("Focus" nil "Focus #." nil "Focus")
+ ("Focus" nil "Focus #." t "Focus")
("From" nil "From #." nil "From")
("Generalizable Variables" nil "Generalizable Variables #." t
"Generalizable\\s-+Variables")
("Generalizable All Variables" nil "Generalizable All Variables." t
"Generalizable\\s-+All\\s-+Variables")
@@ -660,27 +660,26 @@ They deserve a separate menu for sending them to Coq
without insertion.")
("Local Notation" "lnots" "Local Notation # := #." t "Local\\s-+Notation")
("Local Notation (only parsing)" "lnotsp" "Local Notation # := # (only
parsing)." t)
("Notation (simple)" "nots" "Notation # := #." t "Notation")
- ("Typeclasses Opaque" nil "Typeclasses Opaque #." nil
"Typeclasses\\s-+Opaque")
- ("Opaque" nil "Opaque #." nil "Opaque")
+ ("Typeclasses Opaque" nil "Typeclasses Opaque #." t
"Typeclasses\\s-+Opaque")
+ ("Opaque" nil "Opaque #." t "Opaque")
("Obligation Tactic" nil "Obligation Tactic := #." t
"Obligation\\s-+Tactic")
("Local Open Scope" nil "Local Open Scope #" t "Local\\s-+Open\\s-+Scope")
("Open Local Scope" nil "Open Local Scope #" t "Open\\s-+Local\\s-+Scope")
("Open Scope" "opsc" "Open Scope #" t "Open\\s-+Scope")
("Preterm" nil "Preterm." nil "Preterm")
- ("Qed" nil "Qed." nil "Qed")
+ ("Qed" nil "Qed." t "Qed")
("Recursive Extraction" "recextr" "Recursive Extraction @{id}." nil
"Recursive\\s-+Extraction")
("Recursive Extraction Library" "recextrl" "Recursive Extraction Library
@{id}." nil "Recursive\\s-+Extraction\\s-+Library")
("Recursive Extraction Module" "recextrm" "Recursive Extraction Module
@{id}." nil "Recursive\\s-+Extraction\\s-+Module")
- ("Remove Hints" nil "Remove Hints #: #." nil "Remove\\s-+Hints")
- ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath")
- ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath")
+ ("Remove Hints" nil "Remove Hints #: #." t "Remove\\s-+Hints")
+ ("Remove LoadPath" nil "Remove LoadPath" t "Remove\\s-+LoadPath")
("Remove Printing If" nil "Remove Printing If #." t
"Remove\\s-+Printing\\s-+If")
("Remove Printing Let" nil "Remove Printing Let #." t
"Remove\\s-+Printing\\s-+Let")
("Require Export" nil "Require Export #." t "Require\\s-+Export")
("Require Import" nil "Require Import #." t "Require\\s-+Import")
("Require" nil "Require #." t "Require")
- ("Reserved Infix" nil "Reserved Infix" nil "Reserved\\s-+Infix")
- ("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation")
+ ("Reserved Infix" nil "Reserved Infix" t "Reserved\\s-+Infix")
+ ("Reserved Notation" nil "Reserved Notation" t "Reserved\\s-+Notation")
("Reset Extraction Inline" nil "Reset Extraction Inline." t
"Reset\\s-+Extraction\\s-+Inline")
("Save" nil "Save." t "Save")
("Set Asymmetric Patterns" nil "Set Asymmetric Patterns" t "Set
Asymmetric\\s-+Patterns")
@@ -809,9 +808,9 @@ They deserve a separate menu for sending them to Coq
without insertion.")
("Local Strategy" nil "Local Strategy # [#]." t "Local\\s-+Strategy")
("Strategy" nil "Strategy # [#]." t "Strategy")
("Tactic Notation" nil "Tactic Notation # := #." t "Tactic\\s-+Notation")
- ("Transparent" nil "Transparent #." nil "Transparent")
+ ("Transparent" nil "Transparent #." t "Transparent")
- ("Unfocus" nil "Unfocus." nil "Unfocus")
+ ("Unfocus" nil "Unfocus." t "Unfocus")
("Unset Asymmetric Patterns" nil "Unset Asymmetric Patterns" t "Unset
Asymmetric\\s-+Patterns")
("Unset Atomic Load" nil "Unset Atomic Load" t "Unset Atomic\\s-+Load")
("Unset Automatic Coercions Import" nil "Unset Automatic Coercions Import"
t "Unset Automatic\\s-+Coercions\\s-+Import")