diff options
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 fa7b954d9..23996282c 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -172,7 +172,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let nP = lift (i+1+decP) p in let env' = push_rel (n,None,t) env in let t_0 = process_pos env' dep' nP (lift 1 t) in - make_prod_dep (dep or dep') env + make_prod_dep (dep || dep') env (n,t, mkArrow t_0 (process_constr |