diff options
| author | herbelin | 2004-07-11 21:07:05 +0000 |
|---|---|---|
| committer | herbelin | 2004-07-11 21:07:05 +0000 |
| commit | b677b4ef232b8919d9b3bda4917111125def0de7 (patch) | |
| tree | 3bfacbdd47e4bca60f04caca84ffed3c5812b500 | |
| parent | 79215171d1bdc63a4dfd130ed4824a41b1179d80 (diff) | |
Eta-expansion du predicat dans build_indrec (suite)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5887 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/indrec.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index b0f68b67be..3645c49155 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -297,12 +297,12 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) = if dep then (Anonymous,None,depind)::lnames' else lnames' in it_mkLambda_or_LetIn_name env (appvect - (mkRel ((if dep then nar+1 else nar) + dect + j), + (mkRel ((if dep then 1 else 0) + dect + j), extended_rel_vect 0 arsign)) arsign in it_mkLambda_or_LetIn_name env (lambda_create env - (depind,mkCase (ci, lift 1 p, mkRel 1, branches))) + (depind,mkCase (ci, lift (nar+1) p, mkRel 1, branches))) lnames' in let typtyi = |