diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /ide/coq_commands.ml | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'ide/coq_commands.ml')
| -rw-r--r-- | ide/coq_commands.ml | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 3a48fc7d..e4a3ae56 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq_commands.ml 10994 2008-05-26 16:21:31Z jnarboux $ *) +(* $Id$ *) let commands = [ [(* "Abort"; *) @@ -43,7 +43,7 @@ let commands = [ ]; ["End"; "End Silent."; - "Eval"; + "Eval"; "Extract Constant"; "Extract Inductive"; "Extraction Inline"; @@ -84,7 +84,7 @@ let commands = [ ["Parameter"; "Proof."; "Program Definition"; - "Program Fixpoint"; + "Program Fixpoint"; "Program Lemma"; "Program Theorem"; ]; @@ -100,7 +100,7 @@ let commands = [ "Require Export"; "Require Import"; "Reset Extraction Inline"; - "Restore State"; + "Restore State"; ]; [ "Save."; "Scheme"; @@ -155,6 +155,7 @@ let commands = [ ] let state_preserving = [ + "About"; "Check"; "Eval"; "Eval lazy in"; @@ -165,7 +166,7 @@ let state_preserving = [ "Extraction Module"; "Inspect"; "Locate"; - + "Obligations"; "Print"; "Print All."; @@ -191,7 +192,7 @@ let state_preserving = [ "Print Scope"; "Print Scopes."; "Print Section"; - + "Print Table Printing If."; "Print Table Printing Let."; "Print Tables."; @@ -229,7 +230,7 @@ let state_preserving = [ ] -let tactics = +let tactics = [ [ "abstract"; @@ -316,7 +317,7 @@ let tactics = "generalize"; "generalize dependent"; ]; - + [ "hnf"; ]; @@ -415,7 +416,7 @@ let tactics = "trivial"; "try"; ]; - + [ "unfold"; "unfold __ in"; |