summaryrefslogtreecommitdiff
path: root/contrib/interface/showproof.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /contrib/interface/showproof.ml
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'contrib/interface/showproof.ml')
-rw-r--r--contrib/interface/showproof.ml32
1 files changed, 16 insertions, 16 deletions
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index ce2ee1e7..4bec7350 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -156,16 +156,16 @@ let seq_to_lnhyp sign sign' cl =
let rule_is_complex r =
match r with
- Tactic (TacArg (Tacexp t),_) -> true
- | Tactic (TacAtom (_,TacAuto _), _) -> true
- | Tactic (TacAtom (_,TacSymmetry _), _) -> true
+ Nested (Tactic
+ ((TacArg (Tacexp _)
+ |TacAtom (_,(TacAuto _|TacSymmetry _))),_),_) -> true
|_ -> false
;;
let rule_to_ntactic r =
let rt =
(match r with
- Tactic (t,_) -> t
+ Nested(Tactic (t,_),_) -> t
| Prim (Refine h) -> TacAtom (dummy_loc,TacExact h)
| _ -> TacAtom (dummy_loc, TacIntroPattern [])) in
if rule_is_complex r
@@ -234,17 +234,17 @@ let to_nproof sigma osign pf =
(List.map (fun x -> (to_nproof_rec sigma sign x).t_proof)
spfl) in
(match r with
- Tactic (TacAtom (_, TacAuto _),_) ->
- if spfl=[]
- then
- {t_info="to_prove";
- t_goal= {newhyp=[];
- t_concl=concl ntree;
- t_full_concl=ntree.t_goal.t_full_concl;
- t_full_env=ntree.t_goal.t_full_env};
- t_proof= Proof (TacAtom (dummy_loc,TacExtend (dummy_loc,"InfoAuto",[])), [ntree])}
- else ntree
- | _ -> ntree))
+ Nested(Tactic (TacAtom (_, TacAuto _),_),_) ->
+ if spfl=[]
+ then
+ {t_info="to_prove";
+ t_goal= {newhyp=[];
+ t_concl=concl ntree;
+ t_full_concl=ntree.t_goal.t_full_concl;
+ t_full_env=ntree.t_goal.t_full_env};
+ t_proof= Proof (TacAtom (dummy_loc,TacExtend (dummy_loc,"InfoAuto",[])), [ntree])}
+ else ntree
+ | _ -> ntree))
else
{t_info="to_prove";
t_goal=(seq_to_lnhyp oldsign nsign cl);
@@ -725,7 +725,7 @@ let rec nsortrec vl x =
| Case(_,x,t,a)
-> nsortrec vl x
| Cast(x,_, t)-> nsortrec vl t
- | Const c -> nsortrec vl (lookup_constant c vl).const_type
+ | Const c -> nsortrec vl (Typeops.type_of_constant vl c)
| _ -> nsortrec vl (type_of vl Evd.empty x)
;;
let nsort x =