diff options
| author | lmamane | 2008-02-22 13:39:13 +0000 |
|---|---|---|
| committer | lmamane | 2008-02-22 13:39:13 +0000 |
| commit | e8ef565dadd110329f806fa3c281055fcd807440 (patch) | |
| tree | e0f069cb228ee77524800d98c53291014c1a1315 /parsing | |
| parent | 2e67ff1b33d05b9efc020de664f3200f9ff0d479 (diff) | |
Merge with lmamane's private branch:
- New vernac command "Delete"
- New vernac command "Undo To"
- Added a few hooks used by new contrib/interface
- Beta/incomplete version of dependency generation and dumping
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 1 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 1 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 2 | ||||
| -rw-r--r-- | parsing/tactic_printer.mli | 1 |
4 files changed, 5 insertions, 0 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index b564828a57..796636c0e0 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -62,6 +62,7 @@ GEXTEND Gram | IDENT "Proof"; c = lconstr -> VernacExactProof c | IDENT "Undo" -> VernacUndo 1 | IDENT "Undo"; n = natural -> VernacUndo n + | IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo n | IDENT "Focus" -> VernacFocus None | IDENT "Focus"; n = natural -> VernacFocus (Some n) | IDENT "Unfocus" -> VernacUnfocus diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 03c72098c4..5c34f2e884 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -749,6 +749,7 @@ GEXTEND Gram (* Resetting *) | IDENT "Reset"; id = identref -> VernacResetName id + | IDENT "Delete"; id = identref -> VernacRemoveName id | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial | IDENT "Back" -> VernacBack 1 | IDENT "Back"; n = natural -> VernacBack n diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 7e7ea7c56e..0daccbba53 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -417,6 +417,7 @@ let rec pr_vernac = function | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id | VernacResume id -> str"Resume" ++ pr_opt pr_lident id | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i + | VernacUndoTo i -> str"Undo" ++ spc() ++ str"To" ++ pr_intarg i | VernacBacktrack (i,j,k) -> str "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k] | VernacFocus i -> str"Focus" ++ pr_opt int i @@ -446,6 +447,7 @@ let rec pr_vernac = function | VernacCheckGuard -> str"Guarded" (* Resetting *) + | VernacRemoveName id -> str"Remove" ++ spc() ++ pr_lident id | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id | VernacResetInitial -> str"Reset Initial" | VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli index 4e78a96875..842b852959 100644 --- a/parsing/tactic_printer.mli +++ b/parsing/tactic_printer.mli @@ -21,6 +21,7 @@ open Proof_type val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds val pr_rule : rule -> std_ppcmds val pr_tactic : tactic_expr -> std_ppcmds +val pr_proof_instr : Decl_expr.proof_instr -> Pp.std_ppcmds val print_script : bool -> evar_map -> proof_tree -> std_ppcmds val print_treescript : |