diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-05-10 01:30:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-05-10 01:30:04 +0000 |
| commit | 7af1bbb5e411607c20d62e371c22e687baa1d7dd (patch) | |
| tree | 607e60a9f92122907a6ecf5b03e1ffbd121d1e5f | |
| parent | 8b0bab9313d9b26e6c9f132e82473b4db9a4832d (diff) | |
Bug lift de la contrainte au passage du let (bug rapporte par S. Boulme)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1738 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 a8cbe4290..f10973afb 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 637ee8448..c31b57a4a 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 166786750..c06e0d580 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 } |