diff options
| author | herbelin | 2000-10-06 16:08:20 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-06 16:08:20 +0000 |
| commit | 970b4b750486ad8544b5d0a3b2246282690e6c98 (patch) | |
| tree | d8aeeee6133883547e7e30246fcc544e32ae9746 /tactics | |
| parent | ca91e3c69ba2dfed3f8fd24f721873f5d0cd2004 (diff) | |
Correction incompatibilites dans la fn des types des inductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@673 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 6 |
2 files changed, 5 insertions, 5 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index e0a8c85413..c27aeb195e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -566,7 +566,7 @@ let gen_absurdity id gl = let discrimination_pf e (t,t1,t2) discriminator lbeq gls = let env = pf_env gls in let (indt,_) = find_mrectype env (project gls) t in - let arity = Global.mind_arity indt in + let arity = Global.mind_nf_arity indt in let sort = pf_type_of gls (pf_concl gls) in match necessary_elimination (snd (destArity arity)) (destSort sort) with | Type_Type -> @@ -611,7 +611,7 @@ let discr id gls = let discriminator = build_discriminator sigma e_env dirn (mkVar e) sort cpath in let (indt,_) = find_mrectype env sigma t in - let arity = Global.mind_arity indt in + let arity = Global.mind_nf_arity indt in let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq gls in diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 1f78dcb85a..944d826055 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -135,7 +135,7 @@ let match_with_disjunction t = match kind_of_term hdapp with | IsMutInd ind -> let mispec = Global.lookup_mind_specif ind in - let constr_types = mis_lc mispec in + let constr_types = mis_nf_lc mispec in let only_one_arg c = ((nb_prod c) - (mis_nparams mispec)) = 1 in if (array_for_all only_one_arg constr_types) && @@ -162,7 +162,7 @@ let match_with_unit_type t = let (hdapp,args) = decomp_app t in match (kind_of_term hdapp) with | IsMutInd ind -> - let constr_types = Global.mind_lc ind in + let constr_types = Global.mind_nf_lc ind in let nconstr = Global.mind_nconstr ind in let zero_args c = ((nb_prod c) - (Global.mind_nparams ind)) = 0 in if nconstr = 1 && (array_for_all zero_args constr_types) then @@ -185,7 +185,7 @@ let match_with_equation t = let (hdapp,args) = decomp_app t in match (kind_of_term hdapp) with | IsMutInd ind -> - let constr_types = Global.mind_lc ind in + let constr_types = Global.mind_nf_lc ind in let nconstr = Global.mind_nconstr ind in if nconstr = 1 && (is_matching (get_pat refl_rel_pat1) constr_types.(0) || |