diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/printer.ml | 7 | ||||
| -rw-r--r-- | parsing/tactic_printer.ml | 12 |
2 files changed, 8 insertions, 11 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index f777a37edf..dd8264ea77 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -458,6 +458,13 @@ let pr_prim_rule = function | Rename (id1,id2) -> (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) + | 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" + + (* Backwards compatibility *) let prterm = pr_lconstr diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 5eedeec079..c2e0e27fb5 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -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"." @@ -189,9 +184,6 @@ let print_treescript nochange sigma pf = ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ prlist_with_sep pr_fnl (print_script nochange sigma) spfl ) - | Some(Change_evars,[spf]) -> - (if nochange then mt () else pr_change pf.goal ++ fnl ()) ++ - aux spf | Some(r,spfl) -> let indent = if List.length spfl >= 2 then 1 else 0 in (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++ @@ -202,8 +194,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 |