diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 8 | ||||
| -rw-r--r-- | pretyping/typing.ml | 3 |
2 files changed, 5 insertions, 6 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0ffa66d2e3..b25af668c9 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -320,12 +320,10 @@ let rec pretype tycon env isevars lvar lmeta cstr = fst (abs_rel env !isevars name j.utj_val j') | RBinder(loc,BProd,name,c1,c2) -> - let j = pretype_type empty_tycon env isevars lvar lmeta c1 in + let j = pretype_type empty_valcon env isevars lvar lmeta c1 in let var = (name,j.utj_val) in - (* Ici, faudrait appeler pretype_type mais gen_rel n'a pas la bonne - interface, tout ca pour preserver le message d'erreur de gen_rel *) - - let j' = pretype empty_tycon (push_rel_assum var env) isevars lvar lmeta c2 in + let env' = push_rel_assum var env in + let j' = pretype_type empty_valcon env' isevars lvar lmeta c2 in let resj = try fst (gen_rel env !isevars name j j') with TypeError _ as e -> Stdpp.raise_with_loc loc e in diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 3f0ab9501a..8279fb7e89 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -95,7 +95,8 @@ let rec execute mf env sigma cstr = let varj = type_judgment env sigma j in let env1 = push_rel_assum (name,varj.utj_val) env in let j' = execute mf env1 sigma c2 in - let (j,_) = gen_rel env1 sigma name varj j' in + let varj' = type_judgment env sigma j' in + let (j,_) = gen_rel env1 sigma name varj varj' in j | IsLetIn (name,c1,c2,c3) -> |