diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-29 11:29:48 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-29 11:29:48 +0000 |
| commit | c540f6dea7b1a525a4b927a37ffba64d11a8b02a (patch) | |
| tree | 8e7fe9e4bf1881ee566b7c8adbf73dec33796def /pretyping | |
| parent | 52d04b41a0fba7c9649b45f5684a0318b1004c8b (diff) | |
Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1011 85f007b7-540e-0410-9357-904b9bb8a0f7
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 0ffa66d2e..b25af668c 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 3f0ab9501..8279fb7e8 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) -> |