diff options
| author | herbelin | 2003-09-06 14:17:55 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-06 14:17:55 +0000 |
| commit | cb8db3f7af710970a4ddba2fc559910ff7feaffb (patch) | |
| tree | e8f7756f762a7d8abedf4e49e54caa47bf7f985a /pretyping/detyping.ml | |
| parent | d36b4c46cc1cadf73808f4f9e7ef3d1e320c72aa (diff) | |
Mise en place possibilité de définitions locales dans les paramètres des inductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4316 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 01b1bc824f..49034b1b1f 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -202,7 +202,7 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl = let (mib,mip) = Inductive.lookup_mind_specif tenv indsp in let get_consnarg j = let typi = mis_nf_constructor_type (indsp,mib,mip) (j+1) in - let _,t = decompose_prod_n_assum mip.mind_nparams typi in + let _,t = decompose_prod_n_assum (List.length mip.mind_params_ctxt) typi in List.rev (fst (decompose_prod_assum t)) in let consnargs = Array.init (Array.length mip.mind_consnames) get_consnarg in let consnargsl = Array.map List.length consnargs in |