From 0a248d2fe0bb77952c94da34ca097996c0add227 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 19 Feb 2002 10:28:35 +0000
Subject: 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
---
 pretyping/typing.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 5b759e74c6..9a60088322 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
-- 
cgit v1.2.3