summaryrefslogtreecommitdiff
path: root/parsing/tactic_printer.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-02-13 13:48:12 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-02-13 13:48:12 +0000
commit55ce117e8083477593cf1ff2e51a3641c7973830 (patch)
treea82defb4105f175c71b0d13cae42831ce608c4d6 /parsing/tactic_printer.ml
parent208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff)
Imported Upstream version 8.1+dfsgupstream/8.1+dfsg
Diffstat (limited to 'parsing/tactic_printer.ml')
-rw-r--r--parsing/tactic_printer.ml16
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