Adding missing keywords

1 files changed, 327 insertions, 118 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 37867dca..406e4cf3 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -517,6 +517,7 @@ so for the following reasons:
    '(
      ("About" nil "About #." nil "About")
      ("Check" nil "Check" nil "Check")
+     ("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")
@@ -531,133 +532,341 @@ so for the following reasons:
      ("SearchPattern" nil "SearchPattern (#)" nil "SearchPattern")
      ("SearchRewrite" nil "SearchRewrite #" nil "SearchRewrite")
      ("Show" nil "Show #." nil "Show")
-     ("Test" nil "Test" nil "Test" nil t)
-     ("Test Printing Depth" nil "Test Printing Depth." nil "Test\\s-+Printing\\s-+Depth")
-     ("Test Printing If" nil "Test Printing If #." nil "Test\\s-+Printing\\s-+If")
-     ("Test Printing Let" nil "Test Printing Let #." nil "Test\\s-+Printing\\s-+Let")
-     ("Test Printing Synth" nil "Test Printing Synth." nil "Test\\s-+Printing\\s-+Synth")
-     ("Test Printing Width" nil "Test Printing Width." nil "Test\\s-+Printing\\s-+Width")
-     ("Test Printing Wildcard" nil "Test Printing Wildcard." nil "Test\\s-+Printing\\s-+Wildcard")
+     ("Test" nil "Test" nil "Test" nil t) ; let us not highlight all possible options for Test
+     ("Timeout" nil "Timeout" nil "Timeout")
      )
    "Coq queries command, that deserve a separate menu for sending them to coq without insertion. "
    )
 
-
 ;; command that are not declarations, definition or goal starters
 (defvar coq-other-commands-db
-   '(
-     ("Add Parametric Relation" nil "Add Parametric Relation : " t "Add\\s-+Parametric\\s-+Relation")
-     ("BeginSubproof" "bs" "BeginSubproof.\n#\nEndSubproof." t "BeginSubproof")
-     ("EndSubproof" "es" "EndSubproof.#" t "EndSubproof")
-     ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu
-;     ("Add" nil "Add #." nil "Add" nil t)
-     ("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 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 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")
-     ("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t "Arguments\\s-+Scope")
-     ("Arguments" "args" "Arguments @{id} : @{rule}" t "Arguments")
-     ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope")
-     ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure")
-     ("Cd" nil "Cd #." nil "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")
-     ("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")
-     ("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")
-     ("Generalizable Variables" nil "Generalizable Variables #." t "Generalizable\\s-+Variables")
-     ("Generalizable All Variables" nil "Generalizable All Variables." t "Generalizable\\s-+All\\s-+Variables")
-     ("Identity Coercion" nil "Identity Coercion #." t "Identity\\s-+Coercion")
-     ("Implicit Arguments Off" nil "Implicit Arguments Off." t "Implicit\\s-+Arguments\\s-+Off")
-     ("Implicit Arguments On" nil "Implicit Arguments On." t "Implicit\\s-+Arguments\\s-+On")
-     ("Implicit Arguments" nil "Implicit Arguments # [#]." t "Implicit\\s-+Arguments")
-     ("Implicit Types" nil "Implicit Types # : #." t "Implicit\\s-+Types")
-     ("Import" nil "Import #." t "Import")
-     ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix")
-     ("Notation (assoc)" "notas" "Notation \"#\" := # (at level #, # associativity)." t)
-     ("Notation (at assoc)" "notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." t)
-     ("Notation (at at scope)" "notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." t)
-     ("Notation (at at)" "nota" "Notation \"#\" := # (at level #, # at level #)." t)
-     ("Notation (only parsing)" "notsp" "Notation # := # (only parsing)." t)
-     ("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")
-     ("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")
-     ("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 LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath")
-     ("Remove LoadPath" nil "Remove LoadPath" nil "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 Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation")
-     ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline")
-     ("Save" nil "Save." t "Save")
-     ("Set Extraction AutoInline" nil "Set Extraction AutoInline" t "Set\\s-+Extraction\\s-+AutoInline")
-     ("Set Extraction Optimize" nil "Set Extraction Optimize" t "Set\\s-+Extraction\\s-+Optimize")
-     ("Set Implicit Arguments" nil "Set Implicit Arguments" t "Set\\s-+Implicit\\s-+Arguments")
-     ("Set Strict Implicit" nil "Set Strict Implicit" t "Set\\s-+Strict\\s-+Implicit")
-     ("Set Printing Synth" nil "Set Printing Synth" t "Set\\s-+Printing\\s-+Synth")
-     ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set\\s-+Printing\\s-+Wildcard")
-     ("Set Printing All" "sprall" "Set Printing All" t "Set\\s-+Printing\\s-+All")
-     ("Set Hyps Limit" nil "Set Hyps Limit #." nil "Set\\s-+Hyps\\s-+Limit")
-     ("Set Printing Coercions" nil "Set Printing Coercions." t "Set\\s-+Printing\\s-+Coercions")
-     ("Set Printing Notations" "sprn" "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations")
-     ("Set Undo" nil "Set Undo #." nil "Set\\s-+Undo")
-     ("Solve Obligations" "oblssolve" "Solve Obligations using #." t "Solve\\s-+Obligations")
-     ("Tactic Notation" nil "Tactic Notation # := #." t "Tactic\\s-+Notation")
-     ("Transparent" nil "Transparent #." nil "Transparent")
-
-     ("Unfocus" nil "Unfocus." nil "Unfocus")
-     ("Unset Extraction AutoInline" nil "Unset Extraction AutoInline" t "Unset\\s-+Extraction\\s-+AutoInline")
-     ("Unset Extraction Optimize" nil "Unset Extraction Optimize" t "Unset\\s-+Extraction\\s-+Optimize")
-     ("Unset Implicit Arguments" nil "Unset Implicit Arguments" t "Unset\\s-+Implicit\\s-+Arguments")
-     ("Unset Strict Implicit" nil "Unset Strict Implicit" t "Unset\\s-+Strict\\s-+Implicit")
-     ("Unset Printing Synth" nil "Unset Printing Synth" t "Unset\\s-+Printing\\s-+Synth")
-     ("Unset Printing Wildcard" nil "Unset Printing Wildcard" t "Unset\\s-+Printing\\s-+Wildcard")
-     ("Unset Hyps Limit" nil "Unset Hyps Limit" nil "Unset\\s-+Hyps\\s-+Limit")
-     ("Unset Printing All" "unsprall" "Unset Printing All" nil "Unset\\s-+Printing\\s-+All")
-     ("Unset Printing Coercion" nil "Unset Printing Coercion #." t "Unset\\s-+Printing\\s-+Coercion")
-     ("Unset Printing Coercions" nil "Unset Printing Coercions." nil "Unset\\s-+Printing\\s-+Coercions")
-     ("Unset Printing Notations" "unsprn" "Unset Printing Notations" nil "Unset\\s-+Printing\\s-+Notations")
-     ("Unset Undo" nil "Unset Undo." nil "Unset\\s-+Undo")
- ;    ("print" "pr" "print #" "print")
-     )
+  '(
+    ("Add Parametric Relation" nil "Add Parametric Relation : " t "Add\\s-+Parametric\\s-+Relation")
+    ("BeginSubproof" "bs" "BeginSubproof.\n#\nEndSubproof." t "BeginSubproof")
+    ("EndSubproof" "es" "EndSubproof.#" t "EndSubproof")
+    ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu
+                                        ;     ("Add" nil "Add #." nil "Add" nil t)
+    ("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 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 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")
+    ("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t "Arguments\\s-+Scope")
+    ("Arguments" "args" "Arguments @{id} : @{rule}" t "Arguments")
+    ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope")
+    ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure")
+    ("Cd" nil "Cd #." nil "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")
+    ("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")
+    ("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")
+    ("Generalizable Variables" nil "Generalizable Variables #." t "Generalizable\\s-+Variables")
+    ("Generalizable All Variables" nil "Generalizable All Variables." t "Generalizable\\s-+All\\s-+Variables")
+    ("Identity Coercion" nil "Identity Coercion #." t "Identity\\s-+Coercion")
+    ("Implicit Arguments Off" nil "Implicit Arguments Off." t "Implicit\\s-+Arguments\\s-+Off")
+    ("Implicit Arguments On" nil "Implicit Arguments On." t "Implicit\\s-+Arguments\\s-+On")
+    ("Implicit Arguments" nil "Implicit Arguments # [#]." t "Implicit\\s-+Arguments")
+    ("Implicit Types" nil "Implicit Types # : #." t "Implicit\\s-+Types")
+    ("Import" nil "Import #." t "Import")
+    ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix")
+    ("Notation (assoc)" "notas" "Notation \"#\" := # (at level #, # associativity)." t)
+    ("Notation (at assoc)" "notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." t)
+    ("Notation (at at scope)" "notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." t)
+    ("Notation (at at)" "nota" "Notation \"#\" := # (at level #, # at level #)." t)
+    ("Notation (only parsing)" "notsp" "Notation # := # (only parsing)." t)
+    ("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")
+    ("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")
+    ("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 LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath")
+    ("Remove LoadPath" nil "Remove LoadPath" nil "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 Notation" nil "Reserved Notation" nil "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")
+    ("Set Atomic Load" nil "Set Atomic Load" t "Set Atomic\\s-+Load")
+    ("Set Automatic Coercions Import" nil "Set Automatic Coercions Import" t "Set Automatic\\s-+Coercions\\s-+Import")
+    ("Set Automatic Introduction" nil "Set Automatic Introduction" t "Set Automatic\\s-+Introduction")
+    ("Set Boolean Equality Schemes" nil "Set Boolean Equality Schemes" t "Set Boolean\\s-+Equality\\s-+Schemes")
+    ("Set Bracketing Last Introduction Pattern" nil "Set Bracketing Last Introduction Pattern" t "Set Bracketing\\s-+Last\\s-+Introduction\\s-+Pattern")
+    ("Set Bullet Behavior" nil "Set Bullet Behavior" t "Set Bullet\\s-+Behavior")
+    ("Set Case Analysis Schemes" nil "Set Case Analysis Schemes" t "Set Case\\s-+Analysis\\s-+Schemes")
+    ("Set Compat Notations" nil "Set Compat Notations" t "Set Compat\\s-+Notations")
+    ("Set Congruence Depth" nil "Set Congruence Depth" t "Set Congruence\\s-+Depth")
+    ("Set Congruence Verbose" nil "Set Congruence Verbose" t "Set Congruence\\s-+Verbose")
+    ("Set Contextual Implicit" nil "Set Contextual Implicit" t "Set Contextual\\s-+Implicit")
+    ("Set Debug Auto" nil "Set Debug Auto" t "Set Debug\\s-+Auto")
+    ("Set Debug Eauto" nil "Set Debug Eauto" t "Set Debug\\s-+Eauto")
+    ("Set Debug RAKAM" nil "Set Debug RAKAM" t "Set Debug\\s-+RAKAM")
+    ("Set Debug Tactic Unification" nil "Set Debug Tactic Unification" t "Set Debug\\s-+Tactic\\s-+Unification")
+    ("Set Debug Trivial" nil "Set Debug Trivial" t "Set Debug\\s-+Trivial")
+    ("Set Debug Unification" nil "Set Debug Unification" t "Set Debug\\s-+Unification")
+    ("Set Decidable Equality Schemes" nil "Set Decidable Equality Schemes" t "Set Decidable\\s-+Equality\\s-+Schemes")
+    ("Set Default Clearing Used Hypotheses" nil "Set Default Clearing Used Hypotheses" t "Set Default\\s-+Clearing\\s-+Used\\s-+Hypotheses")
+    ("Set Default Goal Selector" nil "Set Default Goal Selector" t "Set Default\\s-+Goal\\s-+Selector")
+    ("Set Default Proof Mode" nil "Set Default Proof Mode" t "Set Default\\s-+Proof\\s-+Mode")
+    ("Set Default Proof Using" nil "Set Default Proof Using" t "Set Default\\s-+Proof\\s-+Using")
+    ("Set Default Timeout" nil "Set Default Timeout" t "Set Default\\s-+Timeout")
+    ("Set Dependent Propositions Elimination" nil "Set Dependent Propositions Elimination" t "Set Dependent\\s-+Propositions\\s-+Elimination")
+    ("Set Discriminate Introduction" nil "Set Discriminate Introduction" t "Set Discriminate\\s-+Introduction")
+    ("Set Dump Bytecode" nil "Set Dump Bytecode" t "Set Dump\\s-+Bytecode")
+    ("Set Elimination Schemes" nil "Set Elimination Schemes" t "Set Elimination\\s-+Schemes")
+    ("Set Equality Scheme" nil "Set Equality Scheme" t "Set Equality\\s-+Scheme")
+    ("Set Extraction AccessOpaque" nil "Set Extraction AccessOpaque" t "Set Extraction\\s-+AccessOpaque")
+    ("Set Extraction AutoInline" nil "Set Extraction AutoInline" t "Set Extraction\\s-+AutoInline")
+    ("Set Extraction Conservative Types" nil "Set Extraction Conservative Types" t "Set Extraction\\s-+Conservative\\s-+Types")
+    ("Set Extraction File Comment" nil "Set Extraction File Comment" t "Set Extraction\\s-+File\\s-+Comment")
+    ("Set Extraction Flag" nil "Set Extraction Flag" t "Set Extraction\\s-+Flag")
+    ("Set Extraction KeepSingleton" nil "Set Extraction KeepSingleton" t "Set Extraction\\s-+KeepSingleton")
+    ("Set Extraction Optimize" nil "Set Extraction Optimize" t "Set Extraction\\s-+Optimize")
+    ("Set Extraction SafeImplicits" nil "Set Extraction SafeImplicits" t "Set Extraction\\s-+SafeImplicits")
+    ("Set Extraction TypeExpand" nil "Set Extraction TypeExpand" t "Set Extraction\\s-+TypeExpand")
+    ("Set Firstorder Depth" nil "Set Firstorder Depth" t "Set Firstorder\\s-+Depth")
+    ("Set Hide Obligations" nil "Set Hide Obligations" t "Set Hide\\s-+Obligations")
+    ("Set Implicit Arguments" nil "Set Implicit Arguments" t "Set Implicit\\s-+Arguments")
+    ("Set Info Auto" nil "Set Info Auto" t "Set Info\\s-+Auto")
+    ("Set Info Eauto" nil "Set Info Eauto" t "Set Info\\s-+Eauto")
+    ("Set Info Level" nil "Set Info Level" t "Set Info\\s-+Level")
+    ("Set Info Trivial" nil "Set Info Trivial" t "Set Info\\s-+Trivial")
+    ("Set Injection L2R Pattern Order" nil "Set Injection L2R Pattern Order" t "Set Injection\\s-+L2R\\s-+Pattern\\s-+Order")
+    ("Set Injection On Proofs" nil "Set Injection On Proofs" t "Set Injection\\s-+On\\s-+Proofs")
+    ("Set Inline Level" nil "Set Inline Level" t "Set Inline\\s-+Level")
+    ("Set Intuition Iff Unfolding" nil "Set Intuition Iff Unfolding" t "Set Intuition\\s-+Iff\\s-+Unfolding")
+    ("Set Intuition Negation Unfolding" nil "Set Intuition Negation Unfolding" t "Set Intuition\\s-+Negation\\s-+Unfolding")
+    ("Set Kernel Term Sharing" nil "Set Kernel Term Sharing" t "Set Kernel\\s-+Term\\s-+Sharing")
+    ("Set Keyed Unification" nil "Set Keyed Unification" t "Set Keyed\\s-+Unification")
+    ("Set Loose Hint Behavior" nil "Set Loose Hint Behavior" t "Set Loose\\s-+Hint\\s-+Behavior")
+    ("Set Maximal Implicit Insertion" nil "Set Maximal Implicit Insertion" t "Set Maximal\\s-+Implicit\\s-+Insertion")
+    ("Set Nonrecursive Elimination Schemes" nil "Set Nonrecursive Elimination Schemes" t "Set Nonrecursive\\s-+Elimination\\s-+Schemes")
+    ("Set Parsing Explicit" nil "Set Parsing Explicit" t "Set Parsing\\s-+Explicit")
+    ("Set Primitive Projections" nil "Set Primitive Projections" t "Set Primitive\\s-+Projections")
+    ("Set Printing All" nil "Set Printing All" t "Set Printing\\s-+All")
+    ("Set Printing Coercions" nil "Set Printing Coercions" t "Set Printing\\s-+Coercions")
+    ("Set Printing Depth" nil "Set Printing Depth" t "Set Printing\\s-+Depth")
+    ("Set Printing Existential Instances" nil "Set Printing Existential Instances" t "Set Printing\\s-+Existential\\s-+Instances")
+    ("Set Printing Implicit" nil "Set Printing Implicit" t "Set Printing\\s-+Implicit")
+    ("Set Printing Implicit Defensive" nil "Set Printing Implicit Defensive" t "Set Printing\\s-+Implicit\\s-+Defensive")
+    ("Set Printing Matching" nil "Set Printing Matching" t "Set Printing\\s-+Matching")
+    ("Set Printing Notations" nil "Set Printing Notations" t "Set Printing\\s-+Notations")
+    ("Set Printing Primitive Projection Compatibility" nil "Set Printing Primitive Projection Compatibility" t "Set Printing\\s-+Primitive\\s-+Projection\\s-+Compatibility")
+    ("Set Printing Primitive Projection Parameters" nil "Set Printing Primitive Projection Parameters" t "Set Printing\\s-+Primitive\\s-+Projection\\s-+Parameters")
+    ("Set Printing Projections" nil "Set Printing Projections" t "Set Printing\\s-+Projections")
+    ("Set Printing Records" nil "Set Printing Records" t "Set Printing\\s-+Records")
+    ("Set Printing Synth" nil "Set Printing Synth" t "Set Printing\\s-+Synth")
+    ("Set Printing Universes" nil "Set Printing Universes" t "Set Printing\\s-+Universes")
+    ("Set Printing Width" nil "Set Printing Width" t "Set Printing\\s-+Width")
+    ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set Printing\\s-+Wildcard")
+    ("Set Program Mode" nil "Set Program Mode" t "Set Program\\s-+Mode")
+    ("Set Proof Using Clear Unused" nil "Set Proof Using Clear Unused" t "Set Proof\\s-+Using\\s-+Clear\\s-+Unused")
+    ("Set Record Elimination Schemes" nil "Set Record Elimination Schemes" t "Set Record\\s-+Elimination\\s-+Schemes")
+    ("Set Refine Instance Mode" nil "Set Refine Instance Mode" t "Set Refine\\s-+Instance\\s-+Mode")
+    ("Set Regular Subst Tactic" nil "Set Regular Subst Tactic" t "Set Regular\\s-+Subst\\s-+Tactic")
+    ("Set Reversible Pattern Implicit" nil "Set Reversible Pattern Implicit" t "Set Reversible\\s-+Pattern\\s-+Implicit")
+    ("Set Rewriting Schemes" nil "Set Rewriting Schemes" t "Set Rewriting\\s-+Schemes")
+    ("Set Short Module Printing" nil "Set Short Module Printing" t "Set Short\\s-+Module\\s-+Printing")
+    ("Set Shrink Obligations" nil "Set Shrink Obligations" t "Set Shrink\\s-+Obligations")
+    ("Set SimplIsCbn" nil "Set SimplIsCbn" t "Set SimplIsCbn")
+    ("Set Standard Proposition Elimination Names" nil "Set Standard Proposition Elimination Names" t "Set Standard\\s-+Proposition\\s-+Elimination\\s-+Names")
+    ("Set Strict Proofs" nil "Set Strict Proofs" t "Set Strict\\s-+Proofs")
+    ("Set Strict Universe Declaration" nil "Set Strict Universe Declaration" t "Set Strict\\s-+Universe\\s-+Declaration")
+    ("Set Strongly Strict Implicit" nil "Set Strongly Strict Implicit" t "Set Strongly\\s-+Strict\\s-+Implicit")
+    ("Set Suggest Proof Using" nil "Set Suggest Proof Using" t "Set Suggest\\s-+Proof\\s-+Using")
+    ("Set Tactic Compat Context" nil "Set Tactic Compat Context" t "Set Tactic\\s-+Compat\\s-+Context")
+    ("Set Tactic Evars Pattern Unification" nil "Set Tactic Evars Pattern Unification" t "Set Tactic\\s-+Evars\\s-+Pattern\\s-+Unification")
+    ("Set Tactic Pattern Unification" nil "Set Tactic Pattern Unification" t "Set Tactic\\s-+Pattern\\s-+Unification")
+    ("Set Transparent Obligations" nil "Set Transparent Obligations" t "Set Transparent\\s-+Obligations")
+    ("Set Typeclass Resolution After Apply" nil "Set Typeclass Resolution After Apply" t "Set Typeclass\\s-+Resolution\\s-+After\\s-+Apply")
+    ("Set Typeclass Resolution For Conversion" nil "Set Typeclass Resolution For Conversion" t "Set Typeclass\\s-+Resolution\\s-+For\\s-+Conversion")
+    ("Set Typeclasses Debug" nil "Set Typeclasses Debug" t "Set Typeclasses\\s-+Debug")
+    ("Set Typeclasses Dependency Order" nil "Set Typeclasses Dependency Order" t "Set Typeclasses\\s-+Dependency\\s-+Order")
+    ("Set Typeclasses Depth" nil "Set Typeclasses Depth" t "Set Typeclasses\\s-+Depth")
+    ("Set Typeclasses Modulo Eta" nil "Set Typeclasses Modulo Eta" t "Set Typeclasses\\s-+Modulo\\s-+Eta")
+    ("Set Typeclasses Strict Resolution" nil "Set Typeclasses Strict Resolution" t "Set Typeclasses\\s-+Strict\\s-+Resolution")
+    ("Set Typeclasses Unique Instances" nil "Set Typeclasses Unique Instances" t "Set Typeclasses\\s-+Unique\\s-+Instances")
+    ("Set Typeclasses Unique Solutions" nil "Set Typeclasses Unique Solutions" t "Set Typeclasses\\s-+Unique\\s-+Solutions")
+    ("Set Universal Lemma Under Conjunction" nil "Set Universal Lemma Under Conjunction" t "Set Universal\\s-+Lemma\\s-+Under\\s-+Conjunction")
+    ("Set Universe Minimization ToSet" nil "Set Universe Minimization ToSet" t "Set Universe\\s-+Minimization\\s-+ToSet")
+    ("Set Universe Polymorphism" nil "Set Universe Polymorphism" t "Set Universe\\s-+Polymorphism")
+    ("Set Verbose Compat Notations" nil "Set Verbose Compat Notations" t "Set Verbose\\s-+Compat\\s-+Notations")
+    ("Set Function_debug" nil "Set Function_debug" t "Set Function_debug")
+    ("Set Function_raw_tcc" nil "Set Function_raw_tcc" t "Set Function_raw_tcc")
+    ("Set Functional Induction Rewrite Dependent" nil "Set Functional Induction Rewrite Dependent" t "Set Functional\\s-+Induction\\s-+Rewrite\\s-+Dependent")
+    ("Set Hyps Limit" nil "Set Hyps Limit" t "Set Hyps\\s-+Limit")
+    ("Set Ltac Debug" nil "Set Ltac Debug" t "Set Ltac\\s-+Debug")
+    ("Set Silent" nil "Set Silent" t "Set Silent")
+    ("Set Undo" nil "Set Undo" t "Set Undo")
+    ("Set Search Blacklist" nil "Set Search Blacklist" t "Set Search\\s-+Blacklist")
+    ("Set Printing Coercion" nil "Set Printing Coercion" t "Set Printing\\s-+Coercion")
+    ("Set Printing If" nil "Set Printing If" t "Set Printing\\s-+If")
+    ("Set Printing Let" nil "Set Printing Let" t "Set Printing\\s-+Let")
+    ("Set Printing Record" nil "Set Printing Record" t "Set Printing\\s-+Record")
+    ("Set Printing Constructor" nil "Set Printing Constructor" t "Set Printing\\s-+Constructor")
+    ("Solve Obligations" "oblssolve" "Solve Obligations using #." t "Solve\\s-+Obligations")
+    ("Tactic Notation" nil "Tactic Notation # := #." t "Tactic\\s-+Notation")
+    ("Transparent" nil "Transparent #." nil "Transparent")
+
+    ("Unfocus" nil "Unfocus." nil "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")
+    ("Unset Automatic Introduction" nil "Unset Automatic Introduction" t "Unset Automatic\\s-+Introduction")
+    ("Unset Boolean Equality Schemes" nil "Unset Boolean Equality Schemes" t "Unset Boolean\\s-+Equality\\s-+Schemes")
+    ("Unset Bracketing Last Introduction Pattern" nil "Unset Bracketing Last Introduction Pattern" t "Unset Bracketing\\s-+Last\\s-+Introduction\\s-+Pattern")
+    ("Unset Bullet Behavior" nil "Unset Bullet Behavior" t "Unset Bullet\\s-+Behavior")
+    ("Unset Case Analysis Schemes" nil "Unset Case Analysis Schemes" t "Unset Case\\s-+Analysis\\s-+Schemes")
+    ("Unset Compat Notations" nil "Unset Compat Notations" t "Unset Compat\\s-+Notations")
+    ("Unset Congruence Depth" nil "Unset Congruence Depth" t "Unset Congruence\\s-+Depth")
+    ("Unset Congruence Verbose" nil "Unset Congruence Verbose" t "Unset Congruence\\s-+Verbose")
+    ("Unset Contextual Implicit" nil "Unset Contextual Implicit" t "Unset Contextual\\s-+Implicit")
+    ("Unset Debug Auto" nil "Unset Debug Auto" t "Unset Debug\\s-+Auto")
+    ("Unset Debug Eauto" nil "Unset Debug Eauto" t "Unset Debug\\s-+Eauto")
+    ("Unset Debug RAKAM" nil "Unset Debug RAKAM" t "Unset Debug\\s-+RAKAM")
+    ("Unset Debug Tactic Unification" nil "Unset Debug Tactic Unification" t "Unset Debug\\s-+Tactic\\s-+Unification")
+    ("Unset Debug Trivial" nil "Unset Debug Trivial" t "Unset Debug\\s-+Trivial")
+    ("Unset Debug Unification" nil "Unset Debug Unification" t "Unset Debug\\s-+Unification")
+    ("Unset Decidable Equality Schemes" nil "Unset Decidable Equality Schemes" t "Unset Decidable\\s-+Equality\\s-+Schemes")
+    ("Unset Default Clearing Used Hypotheses" nil "Unset Default Clearing Used Hypotheses" t "Unset Default\\s-+Clearing\\s-+Used\\s-+Hypotheses")
+    ("Unset Default Goal Selector" nil "Unset Default Goal Selector" t "Unset Default\\s-+Goal\\s-+Selector")
+    ("Unset Default Proof Mode" nil "Unset Default Proof Mode" t "Unset Default\\s-+Proof\\s-+Mode")
+    ("Unset Default Proof Using" nil "Unset Default Proof Using" t "Unset Default\\s-+Proof\\s-+Using")
+    ("Unset Default Timeout" nil "Unset Default Timeout" t "Unset Default\\s-+Timeout")
+    ("Unset Dependent Propositions Elimination" nil "Unset Dependent Propositions Elimination" t "Unset Dependent\\s-+Propositions\\s-+Elimination")
+    ("Unset Discriminate Introduction" nil "Unset Discriminate Introduction" t "Unset Discriminate\\s-+Introduction")
+    ("Unset Dump Bytecode" nil "Unset Dump Bytecode" t "Unset Dump\\s-+Bytecode")
+    ("Unset Elimination Schemes" nil "Unset Elimination Schemes" t "Unset Elimination\\s-+Schemes")
+    ("Unset Equality Scheme" nil "Unset Equality Scheme" t "Unset Equality\\s-+Scheme")
+    ("Unset Extraction AccessOpaque" nil "Unset Extraction AccessOpaque" t "Unset Extraction\\s-+AccessOpaque")
+    ("Unset Extraction AutoInline" nil "Unset Extraction AutoInline" t "Unset Extraction\\s-+AutoInline")
+    ("Unset Extraction Conservative Types" nil "Unset Extraction Conservative Types" t "Unset Extraction\\s-+Conservative\\s-+Types")
+    ("Unset Extraction File Comment" nil "Unset Extraction File Comment" t "Unset Extraction\\s-+File\\s-+Comment")
+    ("Unset Extraction Flag" nil "Unset Extraction Flag" t "Unset Extraction\\s-+Flag")
+    ("Unset Extraction KeepSingleton" nil "Unset Extraction KeepSingleton" t "Unset Extraction\\s-+KeepSingleton")
+    ("Unset Extraction Optimize" nil "Unset Extraction Optimize" t "Unset Extraction\\s-+Optimize")
+    ("Unset Extraction SafeImplicits" nil "Unset Extraction SafeImplicits" t "Unset Extraction\\s-+SafeImplicits")
+    ("Unset Extraction TypeExpand" nil "Unset Extraction TypeExpand" t "Unset Extraction\\s-+TypeExpand")
+    ("Unset Firstorder Depth" nil "Unset Firstorder Depth" t "Unset Firstorder\\s-+Depth")
+    ("Unset Hide Obligations" nil "Unset Hide Obligations" t "Unset Hide\\s-+Obligations")
+    ("Unset Implicit Arguments" nil "Unset Implicit Arguments" t "Unset Implicit\\s-+Arguments")
+    ("Unset Info Auto" nil "Unset Info Auto" t "Unset Info\\s-+Auto")
+    ("Unset Info Eauto" nil "Unset Info Eauto" t "Unset Info\\s-+Eauto")
+    ("Unset Info Level" nil "Unset Info Level" t "Unset Info\\s-+Level")
+    ("Unset Info Trivial" nil "Unset Info Trivial" t "Unset Info\\s-+Trivial")
+    ("Unset Injection L2R Pattern Order" nil "Unset Injection L2R Pattern Order" t "Unset Injection\\s-+L2R\\s-+Pattern\\s-+Order")
+    ("Unset Injection On Proofs" nil "Unset Injection On Proofs" t "Unset Injection\\s-+On\\s-+Proofs")
+    ("Unset Inline Level" nil "Unset Inline Level" t "Unset Inline\\s-+Level")
+    ("Unset Intuition Iff Unfolding" nil "Unset Intuition Iff Unfolding" t "Unset Intuition\\s-+Iff\\s-+Unfolding")
+    ("Unset Intuition Negation Unfolding" nil "Unset Intuition Negation Unfolding" t "Unset Intuition\\s-+Negation\\s-+Unfolding")
+    ("Unset Kernel Term Sharing" nil "Unset Kernel Term Sharing" t "Unset Kernel\\s-+Term\\s-+Sharing")
+    ("Unset Keyed Unification" nil "Unset Keyed Unification" t "Unset Keyed\\s-+Unification")
+    ("Unset Loose Hint Behavior" nil "Unset Loose Hint Behavior" t "Unset Loose\\s-+Hint\\s-+Behavior")
+    ("Unset Maximal Implicit Insertion" nil "Unset Maximal Implicit Insertion" t "Unset Maximal\\s-+Implicit\\s-+Insertion")
+    ("Unset Nonrecursive Elimination Schemes" nil "Unset Nonrecursive Elimination Schemes" t "Unset Nonrecursive\\s-+Elimination\\s-+Schemes")
+    ("Unset Parsing Explicit" nil "Unset Parsing Explicit" t "Unset Parsing\\s-+Explicit")
+    ("Unset Primitive Projections" nil "Unset Primitive Projections" t "Unset Primitive\\s-+Projections")
+    ("Unset Printing All" nil "Unset Printing All" t "Unset Printing\\s-+All")
+    ("Unset Printing Coercions" nil "Unset Printing Coercions" t "Unset Printing\\s-+Coercions")
+    ("Unset Printing Depth" nil "Unset Printing Depth" t "Unset Printing\\s-+Depth")
+    ("Unset Printing Existential Instances" nil "Unset Printing Existential Instances" t "Unset Printing\\s-+Existential\\s-+Instances")
+    ("Unset Printing Implicit" nil "Unset Printing Implicit" t "Unset Printing\\s-+Implicit")
+    ("Unset Printing Implicit Defensive" nil "Unset Printing Implicit Defensive" t "Unset Printing\\s-+Implicit\\s-+Defensive")
+    ("Unset Printing Matching" nil "Unset Printing Matching" t "Unset Printing\\s-+Matching")
+    ("Unset Printing Notations" nil "Unset Printing Notations" t "Unset Printing\\s-+Notations")
+    ("Unset Printing Primitive Projection Compatibility" nil "Unset Printing Primitive Projection Compatibility" t "Unset Printing\\s-+Primitive\\s-+Projection\\s-+Compatibility")
+    ("Unset Printing Primitive Projection Parameters" nil "Unset Printing Primitive Projection Parameters" t "Unset Printing\\s-+Primitive\\s-+Projection\\s-+Parameters")
+    ("Unset Printing Projections" nil "Unset Printing Projections" t "Unset Printing\\s-+Projections")
+    ("Unset Printing Records" nil "Unset Printing Records" t "Unset Printing\\s-+Records")
+    ("Unset Printing Synth" nil "Unset Printing Synth" t "Unset Printing\\s-+Synth")
+    ("Unset Printing Universes" nil "Unset Printing Universes" t "Unset Printing\\s-+Universes")
+    ("Unset Printing Width" nil "Unset Printing Width" t "Unset Printing\\s-+Width")
+    ("Unset Printing Wildcard" nil "Unset Printing Wildcard" t "Unset Printing\\s-+Wildcard")
+    ("Unset Program Mode" nil "Unset Program Mode" t "Unset Program\\s-+Mode")
+    ("Unset Proof Using Clear Unused" nil "Unset Proof Using Clear Unused" t "Unset Proof\\s-+Using\\s-+Clear\\s-+Unused")
+    ("Unset Record Elimination Schemes" nil "Unset Record Elimination Schemes" t "Unset Record\\s-+Elimination\\s-+Schemes")
+    ("Unset Refine Instance Mode" nil "Unset Refine Instance Mode" t "Unset Refine\\s-+Instance\\s-+Mode")
+    ("Unset Regular Subst Tactic" nil "Unset Regular Subst Tactic" t "Unset Regular\\s-+Subst\\s-+Tactic")
+    ("Unset Reversible Pattern Implicit" nil "Unset Reversible Pattern Implicit" t "Unset Reversible\\s-+Pattern\\s-+Implicit")
+    ("Unset Rewriting Schemes" nil "Unset Rewriting Schemes" t "Unset Rewriting\\s-+Schemes")
+    ("Unset Short Module Printing" nil "Unset Short Module Printing" t "Unset Short\\s-+Module\\s-+Printing")
+    ("Unset Shrink Obligations" nil "Unset Shrink Obligations" t "Unset Shrink\\s-+Obligations")
+    ("Unset SimplIsCbn" nil "Unset SimplIsCbn" t "Unset SimplIsCbn")
+    ("Unset Standard Proposition Elimination Names" nil "Unset Standard Proposition Elimination Names" t "Unset Standard\\s-+Proposition\\s-+Elimination\\s-+Names")
+    ("Unset Strict Proofs" nil "Unset Strict Proofs" t "Unset Strict\\s-+Proofs")
+    ("Unset Strict Universe Declaration" nil "Unset Strict Universe Declaration" t "Unset Strict\\s-+Universe\\s-+Declaration")
+    ("Unset Strongly Strict Implicit" nil "Unset Strongly Strict Implicit" t "Unset Strongly\\s-+Strict\\s-+Implicit")
+    ("Unset Suggest Proof Using" nil "Unset Suggest Proof Using" t "Unset Suggest\\s-+Proof\\s-+Using")
+    ("Unset Tactic Compat Context" nil "Unset Tactic Compat Context" t "Unset Tactic\\s-+Compat\\s-+Context")
+    ("Unset Tactic Evars Pattern Unification" nil "Unset Tactic Evars Pattern Unification" t "Unset Tactic\\s-+Evars\\s-+Pattern\\s-+Unification")
+    ("Unset Tactic Pattern Unification" nil "Unset Tactic Pattern Unification" t "Unset Tactic\\s-+Pattern\\s-+Unification")
+    ("Unset Transparent Obligations" nil "Unset Transparent Obligations" t "Unset Transparent\\s-+Obligations")
+    ("Unset Typeclass Resolution After Apply" nil "Unset Typeclass Resolution After Apply" t "Unset Typeclass\\s-+Resolution\\s-+After\\s-+Apply")
+    ("Unset Typeclass Resolution For Conversion" nil "Unset Typeclass Resolution For Conversion" t "Unset Typeclass\\s-+Resolution\\s-+For\\s-+Conversion")
+    ("Unset Typeclasses Debug" nil "Unset Typeclasses Debug" t "Unset Typeclasses\\s-+Debug")
+    ("Unset Typeclasses Dependency Order" nil "Unset Typeclasses Dependency Order" t "Unset Typeclasses\\s-+Dependency\\s-+Order")
+    ("Unset Typeclasses Depth" nil "Unset Typeclasses Depth" t "Unset Typeclasses\\s-+Depth")
+    ("Unset Typeclasses Modulo Eta" nil "Unset Typeclasses Modulo Eta" t "Unset Typeclasses\\s-+Modulo\\s-+Eta")
+    ("Unset Typeclasses Strict Resolution" nil "Unset Typeclasses Strict Resolution" t "Unset Typeclasses\\s-+Strict\\s-+Resolution")
+    ("Unset Typeclasses Unique Instances" nil "Unset Typeclasses Unique Instances" t "Unset Typeclasses\\s-+Unique\\s-+Instances")
+    ("Unset Typeclasses Unique Solutions" nil "Unset Typeclasses Unique Solutions" t "Unset Typeclasses\\s-+Unique\\s-+Solutions")
+    ("Unset Universal Lemma Under Conjunction" nil "Unset Universal Lemma Under Conjunction" t "Unset Universal\\s-+Lemma\\s-+Under\\s-+Conjunction")
+    ("Unset Universe Minimization ToUnset" nil "Unset Universe Minimization ToUnset" t "Unset Universe\\s-+Minimization\\s-+ToUnset")
+    ("Unset Universe Polymorphism" nil "Unset Universe Polymorphism" t "Unset Universe\\s-+Polymorphism")
+    ("Unset Verbose Compat Notations" nil "Unset Verbose Compat Notations" t "Unset Verbose\\s-+Compat\\s-+Notations")
+    ("Unset Function_debug" nil "Unset Function_debug" t "Unset Function_debug")
+    ("Unset Function_raw_tcc" nil "Unset Function_raw_tcc" t "Unset Function_raw_tcc")
+    ("Unset Functional Induction Rewrite Dependent" nil "Unset Functional Induction Rewrite Dependent" t "Unset Functional\\s-+Induction\\s-+Rewrite\\s-+Dependent")
+    ("Unset Hyps Limit" nil "Unset Hyps Limit" t "Unset Hyps\\s-+Limit")
+    ("Unset Ltac Debug" nil "Unset Ltac Debug" t "Unset Ltac\\s-+Debug")
+    ("Unset Silent" nil "Unset Silent" t "Unset Silent")
+    ("Unset Undo" nil "Unset Undo" t "Unset Undo")
+    ("Unset Search Blacklist" nil "Unset Search Blacklist" t "Unset Search\\s-+Blacklist")
+    ("Unset Printing Coercion" nil "Unset Printing Coercion" t "Unset Printing\\s-+Coercion")
+    ("Unset Printing If" nil "Unset Printing If" t "Unset Printing\\s-+If")
+    ("Unset Printing Let" nil "Unset Printing Let" t "Unset Printing\\s-+Let")
+    ("Unset Printing Record" nil "Unset Printing Record" t "Unset Printing\\s-+Record")
+    ("Unset Printing Constructor" nil "Unset Printing Constructor" t "Unset Printing\\s-+Constructor")
+                                        ;    ("print" "pr" "print #" "print")
+    )
    "Command that are not declarations, definition or goal starters."
   )
 
+
 (defvar coq-ssreflect-commands-db
   '(("Unset Strict Implicit" "unsti" nil t "Strict\\s-+Implicit")
     ("Prenex Implicits" "pi" "Prenex Implicits #" t "Prenex\\s-+Implicits")