diff options
| author |  Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
| commit | 55ce117e8083477593cf1ff2e51a3641c7973830 (patch) | |
| tree | a82defb4105f175c71b0d13cae42831ce608c4d6 /parsing/tactic_printer.ml | |
| parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) | |
Imported Upstream version 8.1+dfsgupstream/8.1+dfsg
Diffstat (limited to 'parsing/tactic_printer.ml')
| -rw-r--r-- | parsing/tactic_printer.ml | 16 |
1 files changed, 6 insertions, 10 deletions
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 6ea1c97e..1fef688c 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactic_printer.ml 9244 2006-10-16 17:11:44Z barras $ *) +(* $Id: tactic_printer.ml 9593 2007-02-05 13:58:52Z corbinea $ *) open Pp open Util @@ -39,11 +39,6 @@ let pr_rule = function end | Daimon -> str "<Daimon>" | Decl_proof _ -> str "proof" - | Change_evars -> - (* This is internal tactic and cannot be replayed at user-level. - Function pr_rule_dot below is used when we want to hide - Change_evars *) - str "Evar change" let uses_default_tac = function | Nested(Tactic(_,dflt),_) -> dflt @@ -51,7 +46,7 @@ let uses_default_tac = function (* Does not print change of evars *) let pr_rule_dot = function - | Change_evars -> mt () + | Prim Change_evars -> mt () | r -> pr_rule r ++ if uses_default_tac r then str "..." else str"." @@ -93,7 +88,10 @@ let rec print_decl_script tac_printer nochange sigma pf = else pr_change pf.goal) ++ fnl () - | Some (Daimon,_) -> mt () + | Some (Daimon,[]) -> mt () + | Some (Prim Change_evars,[next]) -> + (* ignore evar changes *) + print_decl_script tac_printer nochange sigma next | Some (Nested(Proof_instr (opened,instr),_) as rule,subprfs) -> begin match instr.instr,subprfs with @@ -213,8 +211,6 @@ let rec print_info_script sigma osign pf = let {evar_hyps=sign; evar_concl=cl} = pf.goal in match pf.ref with | None -> (mt ()) - | Some(Change_evars,[spf]) -> - print_info_script sigma osign spf | Some(r,spfl) -> (pr_rule r ++ match spfl with |