diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-13 10:44:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-13 11:20:28 +0200 |
| commit | 24d0027f0344bca7abce3b8fa8c2a1e42ecf1a00 (patch) | |
| tree | bdde5a56a8e3ca5b0a258ccb68a85caf498fdf56 /pretyping/indrec.ml | |
| parent | 9a4e062c92ad88c894ebbd6e20ee9d1511f24a3f (diff) | |
Providing a -type-in-type option for collapsing the universe hierarchy.
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 |