Merge fixes

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

2 files changed, 9 insertions, 12 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ef65f2d8fe..9d62eeb131 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1857,7 +1857,7 @@ let constr_of_pat env isevars arsign pat avoid =
 		   typ env (substl args liftt, []) ua avoid
 	       in
 	       let args' = arg' :: List.map (lift n') args in
-	       let env' = push_rels sign' env in
+	       let env' = push_rel_context sign' env in
 		 (pat' :: patargs, args', sign' @ sign, env', n' + n, succ m, avoid))
 	    ci.cs_args (List.rev args) ([], [], [], env, 0, 0, avoid)
 	in
@@ -1877,8 +1877,8 @@ let constr_of_pat env isevars arsign pat avoid =
 		let avoid = id :: avoid in
 		let sign, i, avoid =
 		  try
-		    let env = push_rels sign env in
-		    isevars := the_conv_x_leq (push_rels sign env)
+		    let env = push_rel_context sign env in
+		    isevars := the_conv_x_leq (push_rel_context sign env)
 		      (lift (succ m) ty) (lift 1 apptype) !isevars;
 		    let eq_t = mk_eq (lift (succ m) ty)
 		      (mkRel 1) (* alias *)
@@ -2048,7 +2048,7 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
 	   let eqs_rels, arity = decompose_prod_n_assum neqs arity in
 	     eqs_rels @ neqs_rels @ rhs_rels', arity
 	 in
-	 let rhs_env = push_rels rhs_rels' env in
+	 let rhs_env = push_rel_context rhs_rels' env in
 	 let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
 	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
 	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
@@ -2254,7 +2254,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
   in
   let matx = List.rev matx in
   let _ = assert(len = List.length lets) in
-  let env = push_rels lets env in
+  let env = push_rel_context lets env in
   let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
   let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
   let args = List.rev_map (lift len) args in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2bbadfded7..1d5c4d47f4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -183,8 +183,6 @@ let inh_conv_coerce_to_tycon loc env evdref j = function
   | None -> j
   | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t
 
-let push_rels vars env = List.fold_right push_rel vars env
-
 (* used to enforce a name in Lambda when the type constraints itself
    is named, hence possibly dependent *)
 
@@ -208,7 +206,6 @@ let pretype_id loc env sigma (lvar,unbndltacvars) id =
   (* Look for the binder of [id] *)
   try
     let (n,_,typ) = lookup_rel_id id (rel_context env) in
->>>>>>> Second step of integration of Program:
       { uj_val  = mkRel n; uj_type = lift n typ }
   with Not_found ->
     (* Check if [id] is an ltac variable *)
@@ -507,7 +504,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 			    int cs.cs_nargs ++ str " variables.");
 	  let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
             (List.rev nal) cs.cs_args in
-	  let env_f = push_rels fsign env in
+	  let env_f = push_rel_context fsign env in
 	    (* Make dependencies from arity signature impossible *)
 	  let arsgn =
 	    let arsgn,_ = get_arity env indf in
@@ -519,7 +516,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 	  let nar = List.length arsgn in
 	    (match po with
 	     | Some p ->
-		 let env_p = push_rels psign env in
+		 let env_p = push_rel_context psign env in
 		 let pj = pretype_type empty_valcon env_p evdref lvar p in
 		 let ccl = nf_evar !evdref pj.utj_val in
 		 let psign = make_arity_signature env true indf in (* with names *)
@@ -581,7 +578,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 	let psign = (na,None,build_dependent_inductive env indf)::arsgn in
 	let pred,p = match po with
 	  | Some p ->
-	      let env_p = push_rels psign env in
+	      let env_p = push_rel_context psign env in
 	      let pj = pretype_type empty_valcon env_p evdref lvar p in
 	      let ccl = nf_evar !evdref pj.utj_val in
 	      let pred = it_mkLambda_or_LetIn ccl psign in
@@ -610,7 +607,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
                    | Anonymous -> (Name (id_of_string "H"), b, t))
 		cs.cs_args
 	  in
-	  let env_c = push_rels csgn env in
+	  let env_c = push_rel_context csgn env in
 	  let bj = pretype (mk_tycon pi) env_c evdref lvar b in
 	    it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
 	let b1 = f cstrs.(0) b1 in