Skip to content

Commit

Permalink
coq-syntax.el: Fix STATECH booleans (t => the command is not state-pr…
Browse files Browse the repository at this point in the history 
…eserving)
  • Loading branch information
@erikmd
erikmd committed Mar 20, 2023
1 parent 360dc8c commit 7a806e9
Showing 1 changed file with 22 additions and 23 deletions.
45 changes: 22 additions & 23 deletions coq/coq-syntax.el
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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."
Expand All @@ -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")
Expand Down Expand Up @@ -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")
Expand All @@ -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")
Expand Down Expand Up @@ -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")
Expand Down

0 comments on commit 7a806e9

Please sign in to comment.