diff options
| -rw-r--r-- | pretyping/evarutil.ml | 1 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 1 |
3 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index a8cbe4290f..f10973afbb 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -475,3 +475,4 @@ let split_tycon loc env isevars = function let valcon_of_tycon x = x +let lift_tycon = option_app (lift 1) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 637ee8448e..c31b57a4a7 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -61,3 +61,5 @@ val split_tycon : type_constraint * type_constraint val valcon_of_tycon : type_constraint -> val_constraint + +val lift_tycon : type_constraint -> type_constraint diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1667867508..c06e0d5809 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -356,6 +356,7 @@ let rec pretype tycon env isevars lvar lmeta = function | RLetIn(loc,name,c1,c2) -> let j = pretype empty_tycon env isevars lvar lmeta c1 in let var = (name,j.uj_val,j.uj_type) in + let tycon = option_app (lift 1) tycon in let j' = pretype tycon (push_rel_def var env) isevars lvar lmeta c2 in { uj_val = mkLetIn (name, j.uj_val, j.uj_type, j'.uj_val) ; uj_type = type_app (subst1 j.uj_val) j'.uj_type } |