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 0cbfa7597..9f460d08f 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -517,7 +517,7 @@ let weaken_sort_scheme env evd set sort npars term ty = | Prod (n,t,c) -> if Int.equal np 0 then let osort, t' = change_sort_arity sort t in - evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort) !evdref sort osort; + evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort env) !evdref sort osort; mkProd (n, t', c), mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1))) else |