Passage à des contextes de vars et de rels pouvant contenir des déclarations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 3 deletions

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 985b1d3998..0dc0d0a5b8 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -92,7 +92,7 @@ let rec execute mf env sigma cstr =
     | IsLambda (name,c1,c2) -> 
         let j = execute mf env sigma c1 in
 	let var = assumption_of_judgment env sigma j in
-	let env1 = push_rel (name,var) env in
+	let env1 = push_rel_decl (name,var) env in
         let j' = execute mf env1 sigma c2 in 
         let (j,_) = abs_rel env1 sigma name var j' in
 	j
@@ -101,7 +101,7 @@ let rec execute mf env sigma cstr =
         let j = execute mf env sigma c1 in
         let varj = type_judgment env sigma j in
 	let var = assumption_of_type_judgment varj in
-	let env1 = push_rel (name,var) env in
+	let env1 = push_rel_decl (name,var) env in
         let j' = execute mf env1 sigma c2 in
 	let (j,_) = gen_rel env1 sigma name varj j' in
 	j
@@ -119,7 +119,7 @@ and execute_fix mf env sigma lar lfi vdef =
   let nlara = 
     List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
   let env1 = 
-    List.fold_left (fun env nvar -> push_rel nvar env) env nlara in
+    List.fold_left (fun env nvar -> push_rel_decl nvar env) env nlara in
   let vdefj = execute_array mf env1 sigma vdef in
   let vdefv = Array.map j_val_only vdefj in
   let cst3 = type_fixpoint env1 sigma lfi lara vdefj in