diff options
Diffstat (limited to 'contrib/interface/showproof.ml')
| -rw-r--r-- | contrib/interface/showproof.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index c23394e8c..b369bbf31 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -1421,7 +1421,7 @@ and natural_case ig lh g gs ge arg1 ltree with_intros = let targ1 = prod_head (type_of env Evd.empty arg1) in let IndType (indf,targ) = find_rectype env Evd.empty targ1 in let ncti= Array.length(get_constructors env indf) in - let (ind,_) = indf in + let (ind,_) = dest_ind_family indf in let (mib,mip) = lookup_mind_specif env ind in let ti =(string_of_id mip.mind_typename) in let type_arg= targ1 (* List.nth targ (mis_index dmi)*) in @@ -1503,13 +1503,13 @@ and hd_is_mind t ti = try (let env = Global.env() in let IndType (indf,targ) = find_rectype env Evd.empty t in let ncti= Array.length(get_constructors env indf) in - let (ind,_) = indf in + let (ind,_) = dest_ind_family indf in let (mib,mip) = lookup_mind_specif env ind in (string_of_id mip.mind_typename) = ti) with _ -> false and mind_ind_info_hyp_constr indf c = let env = Global.env() in - let (ind,_) = indf in + let (ind,_) = dest_ind_family indf in let (mib,mip) = lookup_mind_specif env ind in let p = mip.mind_nparams in let a = arity_of_constr_of_mind env indf c in @@ -1539,7 +1539,7 @@ and natural_elim ig lh g gs ge arg1 ltree with_intros= let targ1 = prod_head (type_of env Evd.empty arg1) in let IndType (indf,targ) = find_rectype env Evd.empty targ1 in let ncti= Array.length(get_constructors env indf) in - let (ind,_) = indf in + let (ind,_) = dest_ind_family indf in let (mib,mip) = lookup_mind_specif env ind in let ti =(string_of_id mip.mind_typename) in let type_arg=targ1 (* List.nth targ (mis_index dmi) *) in @@ -1589,7 +1589,7 @@ and natural_induction ig lh g gs ge arg1 ltree with_intros= let targ1 = prod_head (type_of env Evd.empty arg1) in let IndType (indf,targ) = find_rectype env Evd.empty targ1 in let ncti= Array.length(get_constructors env indf) in - let (ind,_) = indf in + let (ind,_) = dest_ind_family indf in let (mib,mip) = lookup_mind_specif env ind in let ti =(string_of_id mip.mind_typename) in let type_arg= targ1(*List.nth targ (mis_index dmi)*) in |