diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-02-19 10:28:35 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-02-19 10:28:35 +0000 |
| commit | 0a248d2fe0bb77952c94da34ca097996c0add227 (patch) | |
| tree | ccd9bb64d2690cbec77bc353e6d306f6d46416f3 /pretyping | |
| parent | 474114796be655d2c5191c371876e6bdc3783241 (diff) | |
typage du produit: type_judgment appele avec contexte incorrect
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2488 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 5b759e74c..9a6008832 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -106,8 +106,8 @@ let rec execute mf env sigma cstr = let varj = type_judgment env sigma j in let env1 = push_rel (name,None,varj.utj_val) env in let j' = execute mf env1 sigma c2 in - let varj' = type_judgment env sigma j' in - judge_of_product env1 name varj varj' + let varj' = type_judgment env1 sigma j' in + judge_of_product env name varj varj' | LetIn (name,c1,c2,c3) -> let j1 = execute mf env sigma c1 in |