diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 19:12:08 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 19:12:08 +0000 |
| commit | 95d4aef96fb7b490b188afe66e8345428e9706ee (patch) | |
| tree | 3990c1a6bfce095e941d756df5387b63e86e8353 /pretyping/indrec.ml | |
| parent | ef41c3d1f93e2fa82cbaa97adaa03852e8fcd7b8 (diff) | |
Paramétrisation vis à vis de existential_key
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/indrec.ml')
| -rw-r--r-- | pretyping/indrec.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index ca25938b6..78c23ae61 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -71,7 +71,7 @@ let mis_make_case_com depopt env sigma (ind,mib,mip) kind = let ci = make_default_case_info env RegularStyle ind in let depind = build_dependent_inductive env indf in let deparsign = (Anonymous,None,depind)::lnamesar in - let p = (* mkRel nbprod *) + let p = it_mkLambda_or_LetIn_name env' (appvect (mkRel ((if dep then nbargsprod else mip.mind_nrealargs) + nbprod), |