Uniformisation of the order of arguments env and sigma.

5 files changed, 42 insertions, 42 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index e8e3ef27dc..3c29c5fcbd 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -74,7 +74,7 @@ let type_ctx_instance evars env ctx inst subst =
       let t' = substl subst t in
       let c', l =
 	match b with
-	| None -> interp_casted_constr_evars evars env (List.hd l) t', List.tl l
+	| None -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l
 	| Some b -> substl subst b, l
       in
       let d = na, Some c', t' in
@@ -133,8 +133,8 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
     else tclass 
   in
   let k, u, cty, ctx', ctx, len, imps, subst =
-    let impls, ((env', ctx), imps) = interp_context_evars evars env ctx in
-    let c', imps' = interp_type_evars_impls ~impls evars env' tclass in
+    let impls, ((env', ctx), imps) = interp_context_evars env evars ctx in
+    let c', imps' = interp_type_evars_impls ~impls env' evars tclass in
     let len = List.length ctx in
     let imps = imps @ Impargs.lift_implicits len imps' in
     let ctx', c = decompose_prod_assum c' in
@@ -200,7 +200,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	match props with
 	| None -> if List.is_empty k.cl_props then Some (Inl subst) else None
 	| Some (Inr term) ->
-	    let c = interp_casted_constr_evars evars env' term cty in
+	    let c = interp_casted_constr_evars env' evars term cty in
 	      Some (Inr (c, subst))
 	| Some (Inl props) ->
 	    let get_id =
@@ -327,7 +327,7 @@ let named_of_rel_context l =
 let context poly l =
   let env = Global.env() in
   let evars = ref Evd.empty in
-  let _, ((env', fullctx), impls) = interp_context_evars evars env l in
+  let _, ((env', fullctx), impls) = interp_context_evars env evars l in
   let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in
   let fullctx = Context.map_rel_context subst fullctx in
   let ce t = Evarutil.check_evars env Evd.empty !evars t in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index df07026f6f..74122d1045 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -80,7 +80,7 @@ let red_constant_entry n ce = function
 let interp_definition bl p red_option c ctypopt =
   let env = Global.env() in
   let evdref = ref (Evd.from_env env) in
-  let impls, ((env_bl, ctx), imps1) = interp_context_evars evdref env bl in
+  let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
   let nb_args = List.length ctx in
   let imps,ce =
     match ctypopt with
@@ -88,7 +88,7 @@ let interp_definition bl p red_option c ctypopt =
         let subst = evd_comb0 Evd.nf_univ_variables evdref in
 	let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in
 	let env_bl = push_rel_context ctx env in
-	let c, imps2 = interp_constr_evars_impls ~impls evdref env_bl c in
+	let c, imps2 = interp_constr_evars_impls ~impls env_bl evdref c in
         let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
         let body = nf (it_mkLambda_or_LetIn c ctx) in
 	let vars = Universes.universes_of_constr body in
@@ -97,11 +97,11 @@ let interp_definition bl p red_option c ctypopt =
  	imps1@(Impargs.lift_implicits nb_args imps2),
 	  definition_entry ~univs:(Univ.ContextSet.to_context ctx) ~poly:p body
     | Some ctyp ->
-	let ty, impsty = interp_type_evars_impls ~impls evdref env_bl ctyp in
+	let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
 	let subst = evd_comb0 Evd.nf_univ_variables evdref in
 	let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in
 	let env_bl = push_rel_context ctx env in
-	let c, imps2 = interp_casted_constr_evars_impls ~impls evdref env_bl c ty in
+	let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in
 	let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
 	let body = nf (it_mkLambda_or_LetIn c ctx) in
 	let typ = nf (it_mkProd_or_LetIn ty ctx) in
@@ -233,7 +233,7 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = ma
 
 let interp_assumption evdref env bl c =
   let c = prod_constr_expr c bl in
-  let ty, impls = interp_type_evars_impls evdref env c in
+  let ty, impls = interp_type_evars_impls env evdref c in
   let evd, nf = nf_evars_and_universes !evdref in
   let ctx = Evd.universe_context_set evd in
     ((nf ty, ctx), impls)
@@ -357,10 +357,10 @@ let is_impredicative env u =
   u = Prop Null || 
   (engagement env = Some Declarations.ImpredicativeSet && u = Prop Pos)
 
-let interp_ind_arity evdref env ind =
+let interp_ind_arity env evdref ind =
   let c = intern_gen IsType env ind.ind_arity in
   let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
-  let t, impls = understand_tcc_evars evdref env ~expected_type:IsType c, imps in
+  let t, impls = understand_tcc_evars env evdref ~expected_type:IsType c, imps in
   let pseudo_poly = check_anonymous_type c in
   let () = if not (Reduction.is_arity env t) then
     user_err_loc (constr_loc ind.ind_arity, "", str "Not an arity")
@@ -475,7 +475,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   let env0 = Global.env() in
   let evdref = ref Evd.(from_env env0) in
   let _, ((env_params, ctx_params), userimpls) =
-    interp_context_evars evdref env0 paramsl
+    interp_context_evars env0 evdref paramsl
   in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
 
@@ -484,7 +484,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   let params = List.map (fun (na,_,_) -> out_name na) assums in
 
   (* Interpret the arities *)
-  let arities = List.map (interp_ind_arity evdref env_params) indl in
+  let arities = List.map (interp_ind_arity env_params evdref) indl in
 
   let fullarities = List.map (fun (c, _, _) -> it_mkProd_or_LetIn c ctx_params) arities in
   let env_ar = push_types env0 indnames fullarities in
@@ -502,7 +502,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
      (* Temporary declaration of notations and scopes *)
      List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
      (* Interpret the constructor types *)
-     List.map3 (interp_cstrs evdref env_ar_params impls) mldatas arities indl)
+     List.map3 (interp_cstrs env_ar_params evdref impls) mldatas arities indl)
      () in
 
   (* Try further to solve evars, and instantiate them *)
@@ -723,20 +723,20 @@ type structured_fixpoint_expr = {
   fix_type : constr_expr
 }
 
-let interp_fix_context evdref env isfix fix =
+let interp_fix_context env evdref isfix fix =
   let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
-  let impl_env, ((env', ctx), imps) = interp_context_evars evdref env before in
-  let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env evdref env' after in
+  let impl_env, ((env', ctx), imps) = interp_context_evars env evdref before in
+  let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env env' evdref after in
   let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
     ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
 
 let interp_fix_ccl evdref impls (env,_) fix =
-  interp_type_evars_impls ~impls evdref env fix.fix_type
+  interp_type_evars_impls ~impls env evdref fix.fix_type
 
-let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
+let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
   Option.map (fun body ->
     let env = push_rel_context ctx env_rec in
-    let body = interp_casted_constr_evars evdref env ~impls body ccl in
+    let body = interp_casted_constr_evars env evdref ~impls body ccl in
     it_mkLambda_or_LetIn body ctx) fix.fix_body
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
@@ -828,17 +828,17 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let env = Global.env() in
   let evdref = ref (Evd.from_env env) in
-  let _, ((env', binders_rel), impls) = interp_context_evars evdref env bl in
+  let _, ((env', binders_rel), impls) = interp_context_evars env evdref bl in
   let len = List.length binders_rel in
   let top_env = push_rel_context binders_rel env in
-  let top_arity = interp_type_evars evdref top_env arityc in
+  let top_arity = interp_type_evars top_env evdref arityc in
   let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
   let argtyp, letbinders, make = telescope binders_rel in
   let argname = Id.of_string "recarg" in
   let arg = (Name argname, None, argtyp) in
   let binders = letbinders @ [arg] in
   let binders_env = push_rel_context binders_rel env in
-  let rel, _ = interp_constr_evars_impls evdref env r in
+  let rel, _ = interp_constr_evars_impls env evdref r in
   let () = check_evars_are_solved env Evd.empty !evdref in
   let relty = Typing.type_of env !evdref rel in
   let relargty =
@@ -855,7 +855,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
 	  | _, _ -> error ()
       with e when Errors.noncritical e -> error ()
   in
-  let measure = interp_casted_constr_evars evdref binders_env measure relargty in
+  let measure = interp_casted_constr_evars binders_env evdref measure relargty in
   let wf_rel, wf_rel_fun, measure_fn =
     let measure_body, measure =
       it_mkLambda_or_LetIn measure letbinders,
@@ -909,15 +909,15 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
     let newimpls = Id.Map.singleton recname
       (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
        scopes @ [None]) in
-      interp_casted_constr_evars evdref ~impls:newimpls
-	(push_rel_context ctx env) body (lift 1 top_arity)
+      interp_casted_constr_evars (push_rel_context ctx env) evdref
+        ~impls:newimpls body (lift 1 top_arity)
   in
   let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
   let prop = mkLambda (Name argname, argtyp, top_arity_let) in
   let def =
     mkApp (Universes.constr_of_global (delayed_force fix_sub_ref),
 	  [| argtyp ; wf_rel ;
-	     Evarutil.e_new_evar evdref env 
+	     Evarutil.e_new_evar env evdref
 	       ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
 	     prop |])
   in
@@ -969,7 +969,7 @@ let interp_recursive isfix fixl notations =
   (* Interp arities allowing for unresolved types *)
   let evdref = ref (Evd.from_env env) in
   let fixctxs, fiximppairs, fixannots =
-    List.split3 (List.map (interp_fix_context evdref env isfix) fixl) in
+    List.split3 (List.map (interp_fix_context env evdref isfix) fixl) in
   let fixctximpenvs, fixctximps = List.split fiximppairs in
   let fixccls,fixcclimps = List.split (List.map3 (interp_fix_ccl evdref) fixctximpenvs fixctxs fixl) in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
@@ -1002,7 +1002,7 @@ let interp_recursive isfix fixl notations =
     Metasyntax.with_syntax_protection (fun () ->
       List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
       List.map4
-	(fun fixctximpenv -> interp_fix_body evdref env_rec (Id.Map.fold Id.Map.add fixctximpenv impls))
+	(fun fixctximpenv -> interp_fix_body env_rec evdref (Id.Map.fold Id.Map.add fixctximpenv impls))
 	fixctximpenvs fixctxs fixl fixccls)
       () in
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 2c8fa52b92..ebaa6a9110 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -49,11 +49,11 @@ let _ =
       optread  = (fun () -> !typeclasses_strict);
       optwrite = (fun b -> typeclasses_strict := b); }
 
-let interp_fields_evars evars env impls_env nots l =
+let interp_fields_evars env evars impls_env nots l =
   List.fold_left2
     (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
-      let t', impl = interp_type_evars_impls evars env ~impls t in
-      let b' = Option.map (fun x -> fst (interp_casted_constr_evars_impls evars env ~impls x t')) b in
+      let t', impl = interp_type_evars_impls env evars ~impls t in
+      let b' = Option.map (fun x -> fst (interp_casted_constr_evars_impls env evars ~impls x t')) b in
       let impls =
 	match i with
 	| Anonymous -> impls
@@ -94,11 +94,11 @@ let typecheck_params_and_fields def id t ps nots fs =
 	(function LocalRawDef (b, _) -> error default_binder_kind b
 	   | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls) ps
   in 
-  let impls_env, ((env1,newps), imps) = interp_context_evars evars env0 ps in
+  let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in
   let t' = match t with 
     | Some t -> 
        let env = push_rel_context newps env0 in
-       let s = interp_type_evars evars env ~impls:empty_internalization_env t in
+       let s = interp_type_evars env evars ~impls:empty_internalization_env t in
        let sred = Reductionops.whd_betadeltaiota env !evars s in
 	 (match kind_of_term sred with
 	 | Sort s' -> 
@@ -113,7 +113,7 @@ let typecheck_params_and_fields def id t ps nots fs =
   let fullarity = it_mkProd_or_LetIn t' newps in
   let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
   let env2,impls,newfs,data =
-    interp_fields_evars evars env_ar impls_env nots (binders_of_decls fs)
+    interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs)
   in
   let sigma = 
     Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar Evd.empty !evars in
@@ -316,11 +316,11 @@ let structure_signature ctx =
     match l with [] -> Evd.empty
       | [(_,_,typ)] ->
         let env = Environ.empty_named_context_val in
-        let (evm, _) = Evarutil.new_pure_evar evm env typ in
+        let (evm, _) = Evarutil.new_pure_evar env evm typ in
         evm
       | (_,_,typ)::tl ->
           let env = Environ.empty_named_context_val in
-          let (evm, ev) = Evarutil.new_pure_evar evm env typ in
+          let (evm, ev) = Evarutil.new_pure_evar env evm typ in
 	  let new_tl = Util.List.map_i
 	    (fun pos (n,c,t) -> n,c,
 	       Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) 1 tl in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 33a78110c3..97f7ace0d9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1116,7 +1116,7 @@ let default_env () = {
 
 let vernac_reserve bl =
   let sb_decl = (fun (idl,c) ->
-    let t,ctx = Constrintern.interp_type Evd.empty (Global.env()) c in
+    let t,ctx = Constrintern.interp_type (Global.env()) Evd.empty c in
     let t = Detyping.detype false [] [] Evd.empty t in
     let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
     Reserve.declare_reserved_type idl t)
@@ -1460,7 +1460,7 @@ let get_current_context_of_args = function
 
 let vernac_check_may_eval redexp glopt rc =
   let (sigma, env) = get_current_context_of_args glopt in
-  let sigma', c = interp_open_constr sigma env rc in
+  let sigma', c = interp_open_constr env sigma rc in
   let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in
   Evarconv.check_problems_are_solved env sigma';
   let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
@@ -1490,7 +1490,7 @@ let vernac_declare_reduction locality s r =
 let vernac_global_check c =
   let env = Global.env() in
   let sigma = Evd.from_env env in
-  let c,ctx = interp_constr sigma env c in
+  let c,ctx = interp_constr env sigma c in
   let senv = Global.safe_env() in
   let cstrs = snd (Evd.evar_universe_context_set ctx) in
   let senv = Safe_typing.add_constraints cstrs senv in
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index c8054cf433..c167f9b795 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -182,7 +182,7 @@ let whelp_constr req c =
 
 let whelp_constr_expr req c =
   let (sigma,env)= Lemmas.get_current_context () in
-  let _,c = interp_open_constr sigma env c in
+  let _,c = interp_open_constr env sigma c in
   whelp_constr req c
 
 let whelp_locate s =