diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2010-05-17 11:58:15 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2010-05-17 11:58:15 +0000 |
| commit | 50284c581b68cf50e44d9b48e3fe7180f2d41ea0 (patch) | |
| tree | 1e236a65449178feef02d49f570fa8a937342452 /coq/coq-syntax.el | |
| parent | cbdd9b5f5a42a16f0b8dc5c26d4f8fdd6925f5df (diff) | |
Added a "remember this" window. Experimental.
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 6fe193ed..b918a9a8 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -415,7 +415,7 @@ See also `coq-prog-env' to adjust the environment." ("Inductive (3 args)" "indv3" "Inductive # : # :=\n| # : #\n| # : #\n| # : #." t ) ("Inductive (4 args)" "indv4" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t ) ("Inductive (5 args)" "indv5" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Instance" "instance" "Instance [ # ] => # where \n# := #;\n# := #." t "Instance") + ("Instance" "instance" "Instance #:#.\nProof.\n#End." t "Instance") ("Program Instance" "pinstance" "Program Instance [ # ] => # where \n# := #;\n# := #." t "Program\\s-+Instance") ("Let" "Let" "Let # : # := #." t "Let") ("Ltac" "ltac" "Ltac # := #" t "Ltac") @@ -474,7 +474,6 @@ See also `coq-prog-env' to adjust the environment." ("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 Morphism" nil "Add Morphism #." t "Add\\s-+Morphism") ("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") |