Uniformisation of the order of arguments env and sigma.

44 files changed, 332 insertions, 330 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index cea4cf122..d872110b9 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -91,8 +91,11 @@
   "intros_pattern" and "intros_patterns" is not anymore behaving like
   tactic "intros" on the empty list.
 
-- API of cut tactics changed: cut_intro should be replaced by
-  "enough_tac Anonymous"
+- API of cut tactics changed: for instance, cut_intro should be replaced by
+  "assert_after Anonymous"
+
+- All functions taking an env and a sigma (or an evdref) now takes the
+  env first.
 
 =========================================
 = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d020a5153..66f51b19e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1846,55 +1846,55 @@ let intern_pattern globalenv patt =
 
 (* All evars resolved *)
 
-let interp_gen kind sigma env ?(impls=empty_internalization_env) c =
+let interp_gen kind env sigma ?(impls=empty_internalization_env) c =
   let c = intern_gen kind ~impls env c in
-  understand ~expected_type:kind sigma env c
+  understand ~expected_type:kind env sigma c
 
-let interp_constr sigma env ?(impls=empty_internalization_env) c =
-  interp_gen WithoutTypeConstraint sigma env c
+let interp_constr env sigma ?(impls=empty_internalization_env) c =
+  interp_gen WithoutTypeConstraint env sigma c
 
-let interp_type sigma env ?(impls=empty_internalization_env) c =
-  interp_gen IsType sigma env ~impls c
+let interp_type env sigma ?(impls=empty_internalization_env) c =
+  interp_gen IsType env sigma ~impls c
 
-let interp_casted_constr sigma env ?(impls=empty_internalization_env) c typ =
-  interp_gen (OfType typ) sigma env ~impls c
+let interp_casted_constr env sigma ?(impls=empty_internalization_env) c typ =
+  interp_gen (OfType typ) env sigma ~impls c
 
 (* Not all evars expected to be resolved *)
 
-let interp_open_constr sigma env c =
-  understand_tcc sigma env (intern_constr env c)
+let interp_open_constr env sigma c =
+  understand_tcc env sigma (intern_constr env c)
 
 (* Not all evars expected to be resolved and computation of implicit args *)
 
-let interp_constr_evars_gen_impls evdref
-    env ?(impls=empty_internalization_env) expected_type c =
+let interp_constr_evars_gen_impls env evdref
+    ?(impls=empty_internalization_env) expected_type c =
   let c = intern_gen expected_type ~impls env c in
   let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in
-    understand_tcc_evars evdref env ~expected_type c, imps
+    understand_tcc_evars env evdref ~expected_type c, imps
 
-let interp_constr_evars_impls evdref env ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen_impls evdref env ~impls WithoutTypeConstraint c
+let interp_constr_evars_impls env evdref ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen_impls env evdref ~impls WithoutTypeConstraint c
 
-let interp_casted_constr_evars_impls evdref env ?(impls=empty_internalization_env) c typ =
-  interp_constr_evars_gen_impls evdref env ~impls (OfType typ) c
+let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ =
+  interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c
 
-let interp_type_evars_impls evdref env ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen_impls evdref env ~impls IsType c
+let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen_impls env evdref ~impls IsType c
 
 (* Not all evars expected to be resolved, with side-effect on evars *)
 
-let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) expected_type c =
+let interp_constr_evars_gen env evdref ?(impls=empty_internalization_env) expected_type c =
   let c = intern_gen expected_type ~impls env c in
-  understand_tcc_evars evdref env ~expected_type c
+  understand_tcc_evars env evdref ~expected_type c
 
-let interp_constr_evars evdref env ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen evdref env WithoutTypeConstraint ~impls c
+let interp_constr_evars env evdref ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c
 
-let interp_casted_constr_evars evdref env ?(impls=empty_internalization_env) c typ =
-  interp_constr_evars_gen evdref env ~impls (OfType typ) c
+let interp_casted_constr_evars env evdref ?(impls=empty_internalization_env) c typ =
+  interp_constr_evars_gen env evdref ~impls (OfType typ) c
 
-let interp_type_evars evdref env ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen evdref env IsType ~impls c
+let interp_type_evars env evdref ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen env evdref IsType ~impls c
 
 (* Miscellaneous *)
 
@@ -1921,15 +1921,15 @@ let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
 
 (* Interpret binders and contexts  *)
 
-let interp_binder sigma env na t =
+let interp_binder env sigma na t =
   let t = intern_gen IsType env t in
   let t' = locate_if_isevar (loc_of_glob_constr t) na t in
-  understand ~expected_type:IsType sigma env t'
+  understand ~expected_type:IsType env sigma t'
 
-let interp_binder_evars evdref env na t =
+let interp_binder_evars env evdref na t =
   let t = intern_gen IsType env t in
   let t' = locate_if_isevar (loc_of_glob_constr t) na t in
-  understand_tcc_evars evdref env ~expected_type:IsType t'
+  understand_tcc_evars env evdref ~expected_type:IsType t'
 
 open Environ
 
@@ -1947,7 +1947,7 @@ let intern_context global_level env impl_env binders =
   with InternalizationError (loc,e) ->
     user_err_loc (loc,"internalize", explain_internalization_error e)
 
-let interp_rawcontext_evars evdref env bl =
+let interp_rawcontext_evars env evdref bl =
   let (env, par, _, impls) =
     List.fold_left
       (fun (env,params,n,impls) (na, k, b, t) ->
@@ -1955,7 +1955,7 @@ let interp_rawcontext_evars evdref env bl =
 	    None ->
 	      let t' = locate_if_isevar (loc_of_glob_constr t) na t in
 	      let t =
-                understand_tcc_evars evdref env ~expected_type:IsType t' in
+                understand_tcc_evars env evdref ~expected_type:IsType t' in
 	      let d = (na,None,t) in
 	      let impls =
 		if k == Implicit then
@@ -1965,14 +1965,14 @@ let interp_rawcontext_evars evdref env bl =
 	      in
 		(push_rel d env, d::params, succ n, impls)
 	  | Some b ->
-	      let c = understand_judgment_tcc evdref env b in
+	      let c = understand_judgment_tcc env evdref b in
 	      let d = (na, Some c.uj_val, c.uj_type) in
 		(push_rel d env, d::params, succ n, impls))
       (env,[],1,[]) (List.rev bl)
   in (env, par), impls
 
-let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) evdref env params =
+let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) env evdref params =
   let int_env,bl = intern_context global_level env impl_env params in
-  let x = interp_rawcontext_evars evdref env bl in
+  let x = interp_rawcontext_evars env evdref bl in
   int_env, x
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index b5cad5d28..932c871e5 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -97,41 +97,41 @@ val intern_context : bool -> env -> internalization_env -> local_binder list ->
 
 (** Main interpretation functions expecting evars to be all resolved *)
 
-val interp_constr : evar_map -> env -> ?impls:internalization_env ->
+val interp_constr : env -> evar_map -> ?impls:internalization_env ->
   constr_expr -> constr Evd.in_evar_universe_context
 
-val interp_casted_constr : evar_map -> env -> ?impls:internalization_env ->
+val interp_casted_constr : env -> evar_map -> ?impls:internalization_env ->
   constr_expr -> types -> constr Evd.in_evar_universe_context
 
-val interp_type : evar_map -> env -> ?impls:internalization_env ->
+val interp_type : env -> evar_map -> ?impls:internalization_env ->
   constr_expr -> types Evd.in_evar_universe_context
 
 (** Main interpretation function expecting evars to be all resolved *)
 
-val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
+val interp_open_constr   : env -> evar_map -> constr_expr -> evar_map * constr
 
 (** Accepting unresolved evars *)
 
-val interp_constr_evars : evar_map ref -> env ->
+val interp_constr_evars : env -> evar_map ref ->
   ?impls:internalization_env -> constr_expr -> constr
 
-val interp_casted_constr_evars : evar_map ref -> env ->
+val interp_casted_constr_evars : env -> evar_map ref ->
   ?impls:internalization_env -> constr_expr -> types -> constr
 
-val interp_type_evars : evar_map ref -> env ->
+val interp_type_evars : env -> evar_map ref ->
   ?impls:internalization_env -> constr_expr -> types
 
 (** Accepting unresolved evars and giving back the manual implicit arguments *)
 
-val interp_constr_evars_impls : evar_map ref -> env ->
+val interp_constr_evars_impls : env -> evar_map ref ->
   ?impls:internalization_env -> constr_expr ->
   constr * Impargs.manual_implicits
 
-val interp_casted_constr_evars_impls : evar_map ref -> env ->
+val interp_casted_constr_evars_impls : env -> evar_map ref ->
   ?impls:internalization_env -> constr_expr -> types ->
   constr * Impargs.manual_implicits
 
-val interp_type_evars_impls : evar_map ref -> env ->
+val interp_type_evars_impls : env -> evar_map ref ->
   ?impls:internalization_env -> constr_expr ->
   types * Impargs.manual_implicits
 
@@ -149,25 +149,25 @@ val interp_reference : ltac_sign -> reference -> glob_constr
 
 (** Interpret binders *)
 
-val interp_binder  : evar_map -> env -> Name.t -> constr_expr -> 
+val interp_binder  : env -> evar_map -> Name.t -> constr_expr -> 
   types Evd.in_evar_universe_context
 
-val interp_binder_evars : evar_map ref -> env -> Name.t -> constr_expr -> types
+val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types
 
 (** Interpret contexts: returns extended env and context *)
 
 val interp_context_evars :
   ?global_level:bool -> ?impl_env:internalization_env ->
-  evar_map ref -> env -> local_binder list ->
+  env -> evar_map ref -> local_binder list ->
   internalization_env * ((env * rel_context) * Impargs.manual_implicits)
 
 (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
 (*   (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)
 (*   ?global_level:bool -> ?impl_env:internalization_env -> *)
-(*   evar_map -> env -> local_binder list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
+(*   env -> evar_map -> local_binder list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
   
 (* val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> *)
-(*   evar_map -> env -> local_binder list ->  *)
+(*   env -> evar_map -> local_binder list ->  *)
 (*   internalization_env *  *)
 (*   ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
 
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 2d81194f2..c8a42c293 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -61,7 +61,7 @@ let transl_with_decl env = function
   | CWith_Module ((_,fqid),qid) ->
       WithMod (fqid,lookup_module qid)
   | CWith_Definition ((_,fqid),c) ->
-      WithDef (fqid,fst (interp_constr Evd.empty env c)) (*FIXME*)
+      WithDef (fqid,fst (interp_constr env Evd.empty c)) (*FIXME*)
 
 let loc_of_module = function
   | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc
diff --git a/plugins/Derive/derive.ml b/plugins/Derive/derive.ml
index 26bf18a43..156c9771a 100644
--- a/plugins/Derive/derive.ml
+++ b/plugins/Derive/derive.ml
@@ -34,7 +34,7 @@ let start_deriving f suchthat lemma =
         TCons ( env , sigma , f_type , (fun sigma ef ->
         let env' = Environ.push_named (f , (Some ef) , f_type) env in
         let evdref = ref sigma in
-        let suchthat = Constrintern.interp_type_evars evdref env' suchthat in
+        let suchthat = Constrintern.interp_type_evars env' evdref suchthat in
         TCons ( env' , !evdref , suchthat , (fun sigma _ ->
         TNil sigma))))))
     in
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 541b59920..10d1b6314 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -143,14 +143,14 @@ let intern_proof_instr globs instr=
 
 (* INTERP *)
 
-let interp_justification_items sigma env =
-    Option.map (List.map (fun c -> fst (*FIXME*)(understand sigma env (fst c))))
+let interp_justification_items env sigma =
+    Option.map (List.map (fun c -> fst (*FIXME*)(understand env sigma (fst c))))
 
-let interp_constr check_sort sigma env c =
+let interp_constr check_sort env sigma c =
   if check_sort then
-    fst (understand sigma env ~expected_type:IsType (fst c) (* FIXME *))
+    fst (understand env sigma ~expected_type:IsType (fst c) (* FIXME *))
   else
-    fst (understand sigma env (fst c))
+    fst (understand env sigma (fst c))
 
 let special_whd env =
   let infos=Closure.create_clos_infos Closure.betadeltaiota env in
@@ -172,16 +172,16 @@ let get_eq_typ info env =
   let typ = decompose_eq env (get_last env) in
     typ
 
-let interp_constr_in_type typ sigma env c =
-  fst (understand sigma env (fst c) ~expected_type:(OfType typ))(*FIXME*)
+let interp_constr_in_type typ env sigma c =
+  fst (understand env sigma (fst c) ~expected_type:(OfType typ))(*FIXME*)
 
-let interp_statement interp_it sigma env st =
+let interp_statement interp_it env sigma st =
   {st_label=st.st_label;
-   st_it=interp_it sigma env st.st_it}
+   st_it=interp_it env sigma st.st_it}
 
-let interp_constr_or_thesis check_sort sigma env = function
+let interp_constr_or_thesis check_sort env sigma = function
     Thesis n -> Thesis n
-  | This c -> This (interp_constr check_sort sigma env c)
+  | This c -> This (interp_constr check_sort env sigma c)
 
 let abstract_one_hyp inject h glob =
   match h with
@@ -212,11 +212,11 @@ let rec match_hyps blend names constr = function
       let rhyps,head = match_hyps blend qnames body q in
 	qhyp::rhyps,head
 
-let interp_hyps_gen inject blend sigma env hyps head =
-  let constr= fst(*FIXME*) (understand sigma env (glob_constr_of_hyps inject hyps head)) in
+let interp_hyps_gen inject blend env sigma hyps head =
+  let constr= fst(*FIXME*) (understand env sigma (glob_constr_of_hyps inject hyps head)) in
     match_hyps blend [] constr hyps
 
-let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps glob_prop)
+let interp_hyps env sigma hyps = fst (interp_hyps_gen fst (fun x _ -> x) env sigma hyps glob_prop)
 
 let dummy_prefix= Id.of_string "__"
 
@@ -318,7 +318,7 @@ let rec match_aliases names constr = function
 
 let detype_ground c = Detyping.detype false [] [] Evd.empty c
 
-let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
+let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
   let et,pinfo =
     match info.pm_stack with
 	Per(et,pi,_,_)::_ -> et,pi
@@ -365,7 +365,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
   let term3=List.fold_right let_in_one_alias aliases term2 in
   let term4=List.fold_right prod_one_id loc_ids term3 in
   let term5=List.fold_right prod_one_hyp params term4 in
-  let constr = fst (understand  sigma env term5)(*FIXME*) in
+  let constr = fst (understand env sigma term5)(*FIXME*) in
   let tparams,nam4,rest4 = match_args destProd [] constr params in
   let tpatvars,nam3,rest3 = match_args destProd nam4 rest4 loc_ids in
   let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in
@@ -382,22 +382,22 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
 	     pat_pat=patt;
 	     pat_expr=pat},thyps
 
-let interp_cut interp_it sigma env cut=
-  let nenv,nstat = interp_it sigma env cut.cut_stat in
+let interp_cut interp_it env sigma cut=
+  let nenv,nstat = interp_it env sigma cut.cut_stat in
     {cut with
        cut_stat=nstat;
-       cut_by=interp_justification_items sigma nenv cut.cut_by}
+       cut_by=interp_justification_items nenv sigma cut.cut_by}
 
-let interp_no_bind interp_it sigma env x =
-  env,interp_it sigma env x
+let interp_no_bind interp_it env sigma x =
+  env,interp_it env sigma x
 
-let interp_suffices_clause sigma env (hyps,cot)=
+let interp_suffices_clause env sigma (hyps,cot)=
   let (locvars,_) as res =
     match cot with
 	This (c,_) ->
-	  let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) sigma env hyps c in
+	  let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) env sigma hyps c in
 	  nhyps,This nc
-      | Thesis Plain as th  -> interp_hyps sigma env hyps,th
+      | Thesis Plain as th  -> interp_hyps env sigma hyps,th
       | Thesis (For n) -> error "\"thesis for\" is not applicable here." in
   let push_one hyp env0 =
     match hyp with
@@ -408,9 +408,9 @@ let interp_suffices_clause sigma env (hyps,cot)=
   let nenv = List.fold_right push_one locvars env in
     nenv,res
 
-let interp_casee sigma env = function
-    Real c -> Real (fst (understand sigma env (fst c)))(*FIXME*)
-  | Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) sigma env cut)
+let interp_casee env sigma = function
+    Real c -> Real (fst (understand env sigma (fst c)))(*FIXME*)
+  | Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) env sigma cut)
 
 let abstract_one_arg = function
     (loc,(id,None)) ->
@@ -424,50 +424,50 @@ let abstract_one_arg = function
 let glob_constr_of_fun args body =
   List.fold_right abstract_one_arg args (fst body)
 
-let interp_fun sigma env args body =
-  let constr=fst (*FIXME*) (understand sigma env (glob_constr_of_fun args body)) in
+let interp_fun env sigma args body =
+  let constr=fst (*FIXME*) (understand env sigma (glob_constr_of_fun args body)) in
     match_args destLambda [] constr args
 
-let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = function
-    Pthus i -> Pthus (interp_bare_proof_instr info sigma env i)
-  | Pthen i -> Pthen (interp_bare_proof_instr info sigma env i)
-  | Phence i -> Phence (interp_bare_proof_instr info sigma env i)
+let rec interp_bare_proof_instr info env sigma = function
+    Pthus i -> Pthus (interp_bare_proof_instr info env sigma i)
+  | Pthen i -> Pthen (interp_bare_proof_instr info env sigma i)
+  | Phence i -> Phence (interp_bare_proof_instr info env sigma i)
   | Pcut c -> Pcut (interp_cut
 		      (interp_no_bind (interp_statement
 					 (interp_constr_or_thesis true)))
-		      sigma env c)
+		      env sigma c)
   | Psuffices c ->
-      Psuffices (interp_cut interp_suffices_clause sigma env c)
+      Psuffices (interp_cut interp_suffices_clause env sigma c)
   | Prew (s,c) -> Prew (s,interp_cut
 			  (interp_no_bind (interp_statement
 			     (interp_constr_in_type (get_eq_typ info env))))
-			  sigma env c)
+			  env sigma c)
 
-  | Psuppose hyps -> Psuppose (interp_hyps sigma env hyps)
+  | Psuppose hyps -> Psuppose (interp_hyps env sigma hyps)
   | Pcase (params,pat,hyps) ->
-      let tparams,tpat,thyps = interp_cases info sigma env params pat hyps in
+      let tparams,tpat,thyps = interp_cases info env sigma params pat hyps in
 	Pcase (tparams,tpat,thyps)
   | Ptake witl ->
-      Ptake (List.map (fun c -> fst (*FIXME*) (understand sigma env (fst c))) witl)
-  | Pconsider (c,hyps) -> Pconsider (interp_constr false sigma env c,
-				     interp_hyps sigma env hyps)
-  | Pper (et,c) -> Pper (et,interp_casee sigma env c)
+      Ptake (List.map (fun c -> fst (*FIXME*) (understand env sigma (fst c))) witl)
+  | Pconsider (c,hyps) -> Pconsider (interp_constr false env sigma c,
+				     interp_hyps env sigma hyps)
+  | Pper (et,c) -> Pper (et,interp_casee env sigma c)
   | Pend bt -> Pend bt
   | Pescape -> Pescape
-  | Passume hyps -> Passume (interp_hyps sigma env hyps)
-  | Pgiven hyps -> Pgiven (interp_hyps sigma env hyps)
-  | Plet hyps -> Plet (interp_hyps sigma env hyps)
-  | Pclaim st -> Pclaim (interp_statement (interp_constr true) sigma env st)
-  | Pfocus st -> Pfocus (interp_statement (interp_constr true) sigma env st)
+  | Passume hyps -> Passume (interp_hyps env sigma hyps)
+  | Pgiven hyps -> Pgiven (interp_hyps env sigma hyps)
+  | Plet hyps -> Plet (interp_hyps env sigma hyps)
+  | Pclaim st -> Pclaim (interp_statement (interp_constr true) env sigma st)
+  | Pfocus st -> Pfocus (interp_statement (interp_constr true) env sigma st)
   | Pdefine (id,args,body) ->
-      let nargs,_,nbody = interp_fun sigma env args body in
+      let nargs,_,nbody = interp_fun env sigma args body in
 	Pdefine (id,nargs,nbody)
   | Pcast (id,typ) ->
-      Pcast(id,interp_constr true sigma env typ)
+      Pcast(id,interp_constr true env sigma typ)
 
-let interp_proof_instr info sigma env instr=
+let interp_proof_instr info env sigma instr=
   {emph = instr.emph;
-   instr = interp_bare_proof_instr info sigma env instr.instr}
+   instr = interp_bare_proof_instr info env sigma instr.instr}
 
 
 
diff --git a/plugins/decl_mode/decl_interp.mli b/plugins/decl_mode/decl_interp.mli
index 6fbf5d25c..492964603 100644
--- a/plugins/decl_mode/decl_interp.mli
+++ b/plugins/decl_mode/decl_interp.mli
@@ -12,4 +12,4 @@ open Decl_expr
 
 val intern_proof_instr : glob_sign -> raw_proof_instr -> glob_proof_instr
 val interp_proof_instr : Decl_mode.pm_info ->
-  Evd.evar_map -> Environ.env -> glob_proof_instr -> proof_instr
+  Environ.env -> Evd.evar_map -> glob_proof_instr -> proof_instr
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index c5a474d39..422b7c499 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1278,7 +1278,7 @@ let understand_my_constr c gls =
     | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,None)
     | rc ->  map_glob_constr frob rc
   in
-  Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(Pretyping.OfType (pf_concl gls)) (frob rawc)
+  Pretyping.understand_tcc env (sig_sig gls) ~expected_type:(Pretyping.OfType (pf_concl gls)) (frob rawc)
 
 let my_refine c gls =
   let oc = understand_my_constr c gls in
@@ -1458,7 +1458,7 @@ let do_instr raw_instr pts =
       let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = env} in
       let glob_instr = intern_proof_instr ist raw_instr in
       let instr =
-	interp_proof_instr (get_its_info gl) sigma env glob_instr in
+	interp_proof_instr (get_its_info gl) env sigma glob_instr in
       ignore (Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)))
     else () end;
   postprocess pts raw_instr.instr;
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 9d909fda3..3ea1e9313 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -55,8 +55,8 @@ let pr_glob_proof_instr _ _ _ instr = Empty.abort instr
 let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }=
   Decl_interp.interp_proof_instr 
     (Decl_mode.get_info sigma gl)
-    (sigma)
     (Goal.V82.env sigma gl)
+    (sigma)
 
 let vernac_decl_proof () = 
   let pf = Proof_global.give_me_the_proof () in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 6fd934654..2987ce60a 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -127,7 +127,7 @@ let mk_open_instance id idc gl m t=
 	      GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,None),t1)
 	| _-> anomaly (Pp.str "can't happen") in
   let ntt=try
-    fst (Pretyping.understand evmap env (raux m rawt))(*FIXME*)
+    fst (Pretyping.understand env evmap (raux m rawt))(*FIXME*)
   with e when Errors.noncritical e ->
     error "Untypable instance, maybe higher-order non-prenex quantification" in
     decompose_lam_n_assum m ntt
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index bbb8a96c5..a597e5d45 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -474,9 +474,9 @@ VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF
   [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")"
       "with" "(" ident(id2) ne_ident_list(cl2)  ")" "using" ident(id) ] ->
      [
-       let f1,ctx = Constrintern.interp_constr Evd.empty (Global.env())
+       let f1,ctx = Constrintern.interp_constr (Global.env()) Evd.empty
 	 (CRef (Libnames.Ident (Loc.ghost,id1),None)) in
-       let f2,ctx' = Constrintern.interp_constr Evd.empty (Global.env())
+       let f2,ctx' = Constrintern.interp_constr (Global.env()) Evd.empty
 	 (CRef (Libnames.Ident (Loc.ghost,id2),None)) in
        let f1type = Typing.type_of (Global.env()) Evd.empty f1 in
        let f2type = Typing.type_of (Global.env()) Evd.empty f2 in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 36942636f..6d2274365 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -333,8 +333,8 @@ let raw_push_named (na,raw_value,raw_typ) env =
   match na with
     | Anonymous -> env
     | Name id ->
-	let value = Option.map (fun x-> fst (Pretyping.understand Evd.empty env x)) raw_value in
-	let typ,ctx = Pretyping.understand Evd.empty env ~expected_type:Pretyping.IsType raw_typ in
+	let value = Option.map (fun x-> fst (Pretyping.understand env Evd.empty x)) raw_value in
+	let typ,ctx = Pretyping.understand env Evd.empty ~expected_type:Pretyping.IsType raw_typ in
 	Environ.push_named (id,value,typ) env
 
 
@@ -486,7 +486,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		   a pseudo value "v1 ... vn".
 		   The "value" of this branch is then simply [res]
 		*)
-		let rt_as_constr,ctx = Pretyping.understand Evd.empty env rt in
+		let rt_as_constr,ctx = Pretyping.understand env Evd.empty rt in
 		let rt_typ = Typing.type_of env Evd.empty rt_as_constr in
 		let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) Evd.empty rt_typ in
 		let res = fresh_id args_res.to_avoid "_res" in
@@ -595,7 +595,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	   and combine the two result
 	*)
 	let v_res = build_entry_lc env funnames avoid v in
-	let v_as_constr,ctx = Pretyping.understand Evd.empty env v in
+	let v_as_constr,ctx = Pretyping.understand env Evd.empty v in
 	let v_type = Typing.type_of env Evd.empty v_as_constr in
 	let new_env =
 	  match n with
@@ -611,7 +611,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	let make_discr = make_discr_match brl in
 	build_entry_lc_from_case env funnames make_discr el brl avoid
     | GIf(_,b,(na,e_option),lhs,rhs) ->
-	let b_as_constr,ctx = Pretyping.understand Evd.empty env b in
+	let b_as_constr,ctx = Pretyping.understand env Evd.empty b in
 	let b_typ = Typing.type_of env Evd.empty b_as_constr in
 	let (ind,_) =
 	  try Inductiveops.find_inductive env Evd.empty b_typ
@@ -643,7 +643,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	      )
 	      nal
 	  in
-	  let b_as_constr,ctx = Pretyping.understand Evd.empty env b in
+	  let b_as_constr,ctx = Pretyping.understand env Evd.empty b in
 	  let b_typ = Typing.type_of env Evd.empty b_as_constr in
 	  let (ind,_) =
 	    try Inductiveops.find_inductive env Evd.empty b_typ
@@ -691,7 +691,7 @@ and build_entry_lc_from_case env funname make_discr
 	in
 	let types =
 	  List.map (fun (case_arg,_) ->
-		      let case_arg_as_constr,ctx = Pretyping.understand Evd.empty env case_arg in
+		      let case_arg_as_constr,ctx = Pretyping.understand env Evd.empty case_arg in
 		      Typing.type_of env Evd.empty case_arg_as_constr
 		   ) el
 	in
@@ -896,7 +896,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			let new_t =
 			  mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt])
 			in
-			let t',ctx = Pretyping.understand Evd.empty env new_t in
+			let t',ctx = Pretyping.understand env Evd.empty new_t in
 			let new_env = Environ.push_rel (n,None,t') env in
 			let new_b,id_to_exclude =
 			  rebuild_cons new_env
@@ -916,7 +916,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  try
 		    observe (str "computing new type for eq : " ++ pr_glob_constr rt);
 		    let t' =
-		      try fst (Pretyping.understand Evd.empty env t)(*FIXME*)
+		      try fst (Pretyping.understand env Evd.empty t)(*FIXME*)
                       with e when Errors.noncritical e -> raise Continue
 		    in
 		    let is_in_b = is_free_in id b in
@@ -939,7 +939,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    mkGProd(n,t,new_b),id_to_exclude
 		  with Continue ->
 		    let jmeq = Globnames.IndRef (fst (destInd (jmeq ()))) in
-		    let ty',ctx = Pretyping.understand Evd.empty env ty in
+		    let ty',ctx = Pretyping.understand env Evd.empty ty in
 		    let ind,args' = Inductive.find_inductive env ty' in
 		    let mib,_ = Global.lookup_inductive (fst ind) in
 		    let nparam = mib.Declarations.mind_nparams in
@@ -961,7 +961,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		      GApp(loc1,GRef(loc2,jmeq,None),[ty;GVar(loc3,id);rt_typ;rt])
 		    in
 		    observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
-		    let eq'_as_constr,ctx = Pretyping.understand Evd.empty env eq' in
+		    let eq'_as_constr,ctx = Pretyping.understand env Evd.empty eq' in
 		    observe (str " computing new type for jmeq : done") ;
 		    let new_args =
 		      match kind_of_term eq'_as_constr with
@@ -1011,7 +1011,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		     if is_in_b then b else  replace_var_by_term id rt b
 		    in
 		    let new_env =
-		      let t',ctx = Pretyping.understand Evd.empty env eq' in
+		      let t',ctx = Pretyping.understand env Evd.empty eq' in
 		      Environ.push_rel (n,None,t') env
 		    in
 		    let new_b,id_to_exclude =
@@ -1049,7 +1049,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  else raise Continue
 	      with Continue -> 
 		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
-		let t',ctx = Pretyping.understand Evd.empty env t in
+		let t',ctx = Pretyping.understand env Evd.empty t in
 		let new_env = Environ.push_rel (n,None,t') env in
 		let new_b,id_to_exclude =
 		  rebuild_cons new_env
@@ -1065,7 +1065,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      end
 	    | _ ->
 		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
-		let t',ctx = Pretyping.understand Evd.empty env t in
+		let t',ctx = Pretyping.understand env Evd.empty t in
 		let new_env = Environ.push_rel (n,None,t') env in
 		let new_b,id_to_exclude =
 		  rebuild_cons new_env
@@ -1084,7 +1084,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let new_crossed_types = t :: crossed_types in
 	  observe (str "computing new type for lambda : " ++ pr_glob_constr rt);
-	  let t',ctx = Pretyping.understand Evd.empty env t in
+	  let t',ctx = Pretyping.understand env Evd.empty t in
 	  match n with
 	    | Name id ->
 		let new_env = Environ.push_rel (n,None,t') env in
@@ -1106,7 +1106,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
     | GLetIn(_,n,t,b) ->
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
-	  let t',ctx = Pretyping.understand Evd.empty env t in
+	  let t',ctx = Pretyping.understand env Evd.empty t in
 	  let type_t' = Typing.type_of env Evd.empty t' in
 	  let new_env = Environ.push_rel (n,Some t',type_t') env in
 	  let new_b,id_to_exclude =
@@ -1131,7 +1131,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      args (crossed_types)
 	      depth t
 	  in
-	  let t',ctx = Pretyping.understand Evd.empty env new_t in
+	  let t',ctx = Pretyping.understand env Evd.empty new_t in
 	  let new_env = Environ.push_rel (na,None,t') env in
 	  let new_b,id_to_exclude =
 	    rebuild_cons new_env
@@ -1290,7 +1290,7 @@ let do_build_inductive
     let rel_arities = Array.mapi rel_arity funsargs in
     Util.Array.fold_left2 (fun env rel_name rel_ar ->
 			     Environ.push_named (rel_name,None, 
-						 fst (with_full_print (Constrintern.interp_constr Evd.empty env) rel_ar)) env) env relnames rel_arities
+						 fst (with_full_print (Constrintern.interp_constr env Evd.empty) rel_ar)) env) env relnames rel_arities
   in
   (* and of the real constructors*)
   let constr i res =
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e2273972e..cd35a09a1 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -130,7 +130,7 @@ let rec abstract_glob_constr c = function
       List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl
         (abstract_glob_constr c bl)
 
-let interp_casted_constr_with_implicits sigma env impls c  =
+let interp_casted_constr_with_implicits env sigma impls c  =
   Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
     ~allow_patvar:false c
 
@@ -148,7 +148,7 @@ let build_newrecursive
     List.fold_left
       (fun (env,impls) ((_,recname),bl,arityc,_) ->
         let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
-        let arity,ctx = Constrintern.interp_type sigma env0 arityc in
+        let arity,ctx = Constrintern.interp_type env0 sigma arityc in
 	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in
         (Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls))
       (env0,Constrintern.empty_internalization_env) lnameargsardef in
@@ -157,7 +157,7 @@ let build_newrecursive
     let f (_,bl,_,def) =
       let def = abstract_glob_constr def bl in
       interp_casted_constr_with_implicits
-        sigma rec_sign rec_impls def
+        rec_sign sigma rec_impls def
     in
     States.with_state_protection (List.map f) lnameargsardef
   in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 0117adede..669b77e03 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -51,7 +51,7 @@ let rec substitterm prof t by_t in_u =
 
 let lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl
 
-let understand = Pretyping.understand Evd.empty (Global.env())
+let understand = Pretyping.understand (Global.env()) Evd.empty
 
 (** Operations on names and identifiers *)
 let id_of_name = function
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 8602f0a52..f3096e7a7 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -194,7 +194,7 @@ let (value_f:constr list -> global_reference -> constr) =
 			       Anonymous)],
 	  GVar(d0,v_id)])
     in
-    let body = fst (understand Evd.empty env glob_body)(*FIXME*) in
+    let body = fst (understand env Evd.empty glob_body)(*FIXME*) in
     it_mkLambda_or_LetIn body context
 
 let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) =
@@ -1340,7 +1340,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
 	 	     (fun c ->
 	 		Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST
 	 		  [intros;
-	 		   Simple.apply (fst (interp_constr Evd.empty (Global.env()) c)) (*FIXME*);
+	 		   Simple.apply (fst (interp_constr (Global.env()) Evd.empty c)) (*FIXME*);
 	 		   Tacticals.New.tclCOMPLETE Auto.default_auto
 	 		  ])
 	 	     )
@@ -1461,10 +1461,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
     generate_induction_principle using_lemmas : unit =
   let env = Global.env() in
   let evd = ref (Evd.from_env env) in
-  let function_type = interp_type_evars evd env type_of_f in
+  let function_type = interp_type_evars env evd type_of_f in
   let env = push_named (function_name,None,function_type) env in
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
-  let ty = interp_type_evars evd env ~impls:rec_impls eq in
+  let ty = interp_type_evars env evd ~impls:rec_impls eq in
   let evm, nf = Evarutil.nf_evars_and_universes !evd in
   let equation_lemma_type = nf_betaiotazeta (nf ty) in
   let function_type = nf function_type in
@@ -1492,8 +1492,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in  
   let relation =
     fst (*FIXME*)(interp_constr
-      Evd.empty
       env_with_pre_rec_args
+      Evd.empty
       r)
   in
   let tcc_lemma_name = add_suffix function_name "_tcc" in
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 97936991e..b28f0652d 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -156,11 +156,11 @@ let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
 
 let ic c =
   let env = Global.env() and sigma = Evd.empty in
-  Constrintern.interp_open_constr sigma env c
+  Constrintern.interp_open_constr env sigma c
 
 let ic_unsafe c = (*FIXME remove *)
   let env = Global.env() and sigma = Evd.empty in
-    fst (Constrintern.interp_constr sigma env c)
+    fst (Constrintern.interp_constr env sigma c)
 
 let ty c = Typing.type_of (Global.env()) Evd.empty c
 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 62bfef886..d52f410d2 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -277,7 +277,7 @@ let inductive_template evdref env tmloc ind =
 	match b with
         | None ->
 	    let ty' = substl subst ty in
-	    let e = e_new_evar evdref env ~src:(hole_source n) ty' in
+	    let e = e_new_evar env evdref ~src:(hole_source n) ty' in
 	    (e::subst,e::evarl,n+1)
 	| Some b ->
 	    (substl subst b::subst,evarl,n+1))
@@ -352,7 +352,7 @@ let coerce_to_indtype typing_fun evdref env matx tomatchl =
 (* Utils *)
 
 let mkExistential env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) evdref =
-  let e, u = e_new_type_evar evdref univ_flexible_alg env ~src:src in e
+  let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in e
 
 let evd_comb2 f evdref x y =
   let (evd',y) = f !evdref x y in
@@ -1574,7 +1574,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
 	    (fun i _ ->
               try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
               1 (rel_context env) in
-        let ev = e_new_evar evdref env ~src:(loc, Evar_kinds.CasesType) ty in
+        let ev = e_new_evar env evdref ~src:(loc, Evar_kinds.CasesType) ty in
         evdref := add_conv_pb (Reduction.CONV,env,substl inst ev,t) !evdref;
         ev
     | _ ->
@@ -1603,7 +1603,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
       let filter = Filter.make (rel_filter @ named_filter) in
       let candidates = u :: List.map mkRel vl in
       let ev =
-	e_new_evar evdref extenv ~src:(loc, Evar_kinds.CasesType)
+	e_new_evar extenv evdref ~src:(loc, Evar_kinds.CasesType)
 	  ~filter ~candidates ty in
       lift k ev
   in
@@ -1617,7 +1617,7 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t =
 	let n = rel_context_length (rel_context env) in
 	let n' = rel_context_length (rel_context tycon_env) in
 	let impossible_case_type, u =
-	  e_new_type_evar evdref univ_flexible_alg env ~src:(loc,Evar_kinds.ImpossibleCase) in
+	  e_new_type_evar env evdref univ_flexible_alg ~src:(loc,Evar_kinds.ImpossibleCase) in
 	(lift (n'-n) impossible_case_type, mkSort u)
     | Some t ->
         let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in
@@ -1858,7 +1858,7 @@ let prepare_predicate_from_arsign_tycon loc tomatchs arsign c =
  * tycon to make the predicate if it is not closed.
  *)
 
-let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
+let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
   let preds =
     match pred, tycon with
     (* No type annotation *)
@@ -1878,7 +1878,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
 	| Some t -> sigma,t
 	| None -> 
 	  let sigma, (t, _) = 
-	    new_type_evar univ_flexible_alg sigma env ~src:(loc, Evar_kinds.CasesType) in
+	    new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType) in
 	    sigma, t
 	in
         (* First strategy: we build an "inversion" predicate *)
@@ -2439,7 +2439,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
      with the type of arguments to match; if none is provided, we
      build alternative possible predicates *)
   let arsign = extract_arity_signature env tomatchs tomatchl in
-  let preds = prepare_predicate loc typing_fun !evdref env tomatchs arsign tycon predopt in
+  let preds = prepare_predicate loc typing_fun env !evdref tomatchs arsign tycon predopt in
 
   let compile_for_one_predicate (sigma,nal,pred) =
     (* We push the initial terms to match and push their alias to rhs' envs *)
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index e51055cef..3ff1d8659 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -114,8 +114,8 @@ val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment
 val prepare_predicate :            Loc.t ->
            (Evarutil.type_constraint ->
             Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) ->
-           Evd.evar_map ->
            Environ.env ->
+           Evd.evar_map ->
            (Term.types * tomatch_type) list ->
            Context.rel_context list ->
            Constr.constr option ->
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index dfaff327a..a1279c1f2 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -81,7 +81,7 @@ let inh_pattern_coerce_to loc pat ind1 ind2 =
 open Program
 
 let make_existential loc ?(opaque = Evar_kinds.Define true) env evdref c =
-  Evarutil.e_new_evar evdref env ~src:(loc, Evar_kinds.QuestionMark opaque) c
+  Evarutil.e_new_evar env evdref ~src:(loc, Evar_kinds.QuestionMark opaque) c
 
 let app_opt env evdref f t =
   whd_betaiota !evdref (app_opt f t)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 190a025ac..d125a799b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -763,7 +763,7 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1),
 	      (i,t2::ks, m-1, test)
 	  else
 	    let dloc = (Loc.ghost,Evar_kinds.InternalHole) in
-            let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
+            let (i',ev) = new_evar env i ~src:dloc (substl ks b) in
 	    (i', ev :: ks, m - 1,test))
 	(evd,[],List.length bs - 1,fun i -> Success i) bs
     in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 9f5de8c90..631438ddf 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1150,7 +1150,7 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar
 	else
 	  let evd, k = Evd.new_sort_variable univ_flexible_alg evd in
 	  let evd, ev3 = 
-	    Evarutil.new_pure_evar evd (Evd.evar_hyps evi) 
+	    Evarutil.new_pure_evar (Evd.evar_hyps evi) evd
 	      ~src:evi.evar_source ~filter:evi.evar_filter 
 	      ?candidates:evi.evar_candidates (it_mkProd_or_LetIn (mkSort k) ctx) 
 	  in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 306032ed9..ddc1ece96 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -351,7 +351,7 @@ let new_pure_evar_full evd evi =
   let evd = Evd.add evd evk evi in
   (evd, evk)
 
-let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates ?store typ =
+let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store typ =
   let newevk = new_untyped_evar() in
   let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store evd in
   (evd,newevk)
@@ -359,12 +359,12 @@ let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates ?store typ
 let new_evar_instance sign evd typ ?src ?filter ?candidates ?store instance =
   assert (not !Flags.debug ||
             List.distinct (ids_of_named_context (named_context_of_val sign)));
-  let evd,newevk = new_pure_evar evd sign ?src ?filter ?candidates ?store typ in
+  let evd,newevk = new_pure_evar sign evd ?src ?filter ?candidates ?store typ in
   (evd,mkEvar (newevk,Array.of_list instance))
 
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
-let new_evar evd env ?src ?filter ?candidates ?store typ =
+let new_evar env evd ?src ?filter ?candidates ?store typ =
   let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
   let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in
   let instance =
@@ -373,13 +373,13 @@ let new_evar evd env ?src ?filter ?candidates ?store typ =
     | Some filter -> Filter.filter_list filter instance in
   new_evar_instance sign evd typ' ?src ?filter ?candidates ?store instance
 
-let new_type_evar ?src ?filter rigid evd env =
+let new_type_evar env evd ?src ?filter rigid =
   let evd', s = new_sort_variable rigid evd in
-  let evd', e = new_evar evd' env ?src ?filter (mkSort s) in
+  let evd', e = new_evar env evd' ?src ?filter (mkSort s) in
     evd', (e, s)
 
-let e_new_type_evar evdref ?src ?filter rigid env =
-  let evd', c = new_type_evar ?src ?filter rigid !evdref env in
+let e_new_type_evar env evdref ?src ?filter rigid =
+  let evd', c = new_type_evar env !evdref ?src ?filter rigid in
     evdref := evd';
     c
 
@@ -392,8 +392,8 @@ let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
     evdref := evd'; mkSort s
 
   (* The same using side-effect *)
-let e_new_evar evdref env ?(src=default_source) ?filter ?candidates ?store ty =
-  let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ?store ty in
+let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ty =
+  let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ty in
   evdref := evd';
   ev
 
@@ -482,7 +482,7 @@ let rec check_and_clear_in_constr evdref err ids c =
             if Id.Map.is_empty rids then c
             else
 	      let env = Context.fold_named_context push_named nhyps ~init:(empty_env) in
-	      let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
+	      let ev'= e_new_evar env evdref ~src:(evar_source evk !evdref) nconcl in
 	      evdref := Evd.define evk ev' !evdref;
 	      let (evk',_) = destEvar ev' in
 	    (* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
@@ -704,17 +704,17 @@ let define_pure_evar_as_product evd evk =
   let evenv = evar_env evi in
   let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
   let s = destSort evi.evar_concl in
-  let evd1,(dom,u1) = new_type_evar univ_flexible_alg evd evenv ~filter:(evar_filter evi) in
+  let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
   let evd2,rng =
     let newenv = push_named (id, None, dom) evenv in
     let src = evar_source evk evd1 in
     let filter = Filter.extend 1 (evar_filter evi) in
       if is_prop_sort s then
        (* Impredicative product, conclusion must fall in [Prop]. *)
-        new_evar evd1 newenv evi.evar_concl ~src ~filter
+        new_evar newenv evd1 evi.evar_concl ~src ~filter
       else
 	let evd3, (rng, srng) =
-	  new_type_evar univ_flexible_alg evd1 newenv ~src ~filter in
+	  new_type_evar newenv evd1 univ_flexible_alg ~src ~filter in
 	let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
 	let evd3 = Evd.set_leq_sort evd3 (Type prods) s in
 	  evd3, rng
@@ -757,7 +757,7 @@ let define_pure_evar_as_lambda env evd evk =
   let newenv = push_named (id, None, dom) evenv in
   let filter = Filter.extend 1 (evar_filter evi) in
   let src = evar_source evk evd1 in
-  let evd2,body = new_evar evd1 newenv ~src (subst1 (mkVar id) rng) ~filter in
+  let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
   let lam = mkLambda (Name id, dom, subst_var id body) in
   Evd.define evk lam evd2, lam
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 2d3dd33a3..081c41560 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -22,28 +22,28 @@ val mk_new_meta : unit -> constr
 
 (** {6 Creating a fresh evar given their type and context} *)
 val new_evar :
-  evar_map -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t -> types -> evar_map * constr
 
 val new_pure_evar :
-  evar_map -> named_context_val -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  named_context_val -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t -> types -> evar_map * evar
 
 val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar
 
 (** the same with side-effects *)
 val e_new_evar :
-  evar_map ref -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t -> types -> constr
 
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
-  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> rigid -> evar_map -> env -> 
+  env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> rigid ->
   evar_map * (constr * sorts)
 
-val e_new_type_evar : evar_map ref ->
-  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> rigid -> env -> constr * sorts
+val e_new_type_evar : env -> evar_map ref ->
+  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> rigid -> constr * sorts
 
 val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
 val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a21548d57..0115f67d5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -364,9 +364,9 @@ let pretype_sort evdref = function
   | GSet -> judge_of_set
   | GType s -> evd_comb1 judge_of_Type evdref s
 
-let new_type_evar evdref env loc =
+let new_type_evar env evdref loc =
   let e, s = 
-    evd_comb0 (fun evd -> Evarutil.new_type_evar univ_flexible_alg evd env ~src:(loc,Evar_kinds.InternalHole)) evdref
+    evd_comb0 (fun evd -> Evarutil.new_type_evar env evd univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
   in e
 
 let get_projection env cst =
@@ -426,24 +426,24 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     let ty =
       match tycon with
       | Some ty -> ty
-      | None -> new_type_evar evdref env loc in
+      | None -> new_type_evar env evdref loc in
     let k = Evar_kinds.MatchingVar (someta,n) in
-      { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
+      { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
 
   | GHole (loc, k, None) ->
       let ty =
         match tycon with
         | Some ty -> ty
         | None ->
-          new_type_evar evdref env loc in
-        { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
+          new_type_evar env evdref loc in
+        { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
 
   | GHole (loc, k, Some arg) ->
       let ty =
         match tycon with
         | Some ty -> ty
         | None ->
-          new_type_evar evdref env loc in
+          new_type_evar env evdref loc in
       let ist = lvar.ltac_genargs in
       let (c, sigma) = Hook.get f_genarg_interp ty env !evdref ist arg in
       let () = evdref := sigma in
@@ -543,7 +543,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	let ctx = smash_rel_context (Inductiveops.inductive_paramdecls ind) in
 	  List.fold_right (fun (n, b, ty) (* par  *)args ->
 	    let ty = substl args ty in
-	    let ev = e_new_evar evdref env ~src:(loc,k) ty in
+	    let ev = e_new_evar env evdref ~src:(loc,k) ty in
 	      ev :: args) ctx []
       in (ind, List.rev args)
     in
@@ -830,7 +830,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	| None ->
 	  let p = match tycon with
 	    | Some ty -> ty
-	    | None -> new_type_evar evdref env loc
+	    | None -> new_type_evar env evdref loc
 	  in
 	    it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
       let pred = nf_evar !evdref pred in
@@ -929,7 +929,7 @@ and pretype_type resolve_tc valcon env evdref lvar = function
 	       utj_type = s }
        | None ->
 	   let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in
-	     { utj_val = e_new_evar evdref env ~src:(loc, knd) (mkSort s);
+	     { utj_val = e_new_evar env evdref ~src:(loc, knd) (mkSort s);
 	       utj_type = s})
   | c ->
       let j = pretype resolve_tc empty_tycon env evdref lvar c in
@@ -943,7 +943,7 @@ and pretype_type resolve_tc valcon env evdref lvar = function
 	      error_unexpected_type_loc
                 (loc_of_glob_constr c) env !evdref tj.utj_val v
 
-let ise_pretype_gen flags sigma env lvar kind c =
+let ise_pretype_gen flags env sigma lvar kind c =
   let evdref = ref sigma in
   let c' = match kind with
     | WithoutTypeConstraint ->
@@ -984,7 +984,7 @@ let on_judgment f j =
   let (c,_,t) = destCast (f c) in
   {uj_val = c; uj_type = t}
 
-let understand_judgment sigma env c =
+let understand_judgment env sigma c =
   let evdref = ref sigma in
   let j = pretype true empty_tycon env evdref empty_lvar c in
   let j = on_judgment (fun c ->
@@ -992,14 +992,14 @@ let understand_judgment sigma env c =
       evdref := evd; c) j
   in j, Evd.evar_universe_context !evdref
 
-let understand_judgment_tcc evdref env c =
+let understand_judgment_tcc env evdref c =
   let j = pretype true empty_tycon env evdref empty_lvar c in
   on_judgment (fun c ->
     let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in
     evdref := evd; c) j
 
-let ise_pretype_gen_ctx flags sigma env lvar kind c =
-  let evd, c = ise_pretype_gen flags sigma env lvar kind c in
+let ise_pretype_gen_ctx flags env sigma lvar kind c =
+  let evd, c = ise_pretype_gen flags env sigma lvar kind c in
   let evd, f = Evarutil.nf_evars_and_universes evd in
     f c, Evd.evar_universe_context evd
 
@@ -1008,16 +1008,16 @@ let ise_pretype_gen_ctx flags sigma env lvar kind c =
 let understand
     ?(flags=all_and_fail_flags)
     ?(expected_type=WithoutTypeConstraint)
-    sigma env c =
-  ise_pretype_gen_ctx flags sigma env empty_lvar expected_type c
+    env sigma c =
+  ise_pretype_gen_ctx flags env sigma empty_lvar expected_type c
 
-let understand_tcc ?(flags=all_no_fail_flags) sigma env ?(expected_type=WithoutTypeConstraint) c =
-  ise_pretype_gen flags sigma env empty_lvar expected_type c
+let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c =
+  ise_pretype_gen flags env sigma empty_lvar expected_type c
 
-let understand_tcc_evars ?(flags=all_no_fail_flags) evdref env ?(expected_type=WithoutTypeConstraint) c =
-  let sigma, c = ise_pretype_gen flags !evdref env empty_lvar expected_type c in
+let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=WithoutTypeConstraint) c =
+  let sigma, c = ise_pretype_gen flags env !evdref empty_lvar expected_type c in
   evdref := sigma;
   c
 
-let understand_ltac flags sigma env lvar kind c =
-  ise_pretype_gen flags sigma env lvar kind c
+let understand_ltac flags env sigma lvar kind c =
+  ise_pretype_gen flags env sigma lvar kind c
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 695b2b51f..5df4c8372 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -70,10 +70,10 @@ val allow_anonymous_refs : bool ref
     unresolved holes as evars and returning the typing contexts of
     these evars. Work as [understand_gen] for the rest. *)
 
-val understand_tcc : ?flags:inference_flags -> evar_map -> env ->
+val understand_tcc : ?flags:inference_flags -> env -> evar_map ->
   ?expected_type:typing_constraint -> glob_constr -> open_constr
 
-val understand_tcc_evars : ?flags:inference_flags -> evar_map ref -> env ->
+val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref ->
   ?expected_type:typing_constraint -> glob_constr -> constr
 
 (** More general entry point with evars from ltac *)
@@ -89,21 +89,21 @@ val understand_tcc_evars : ?flags:inference_flags -> evar_map ref -> env ->
 *)
 
 val understand_ltac : inference_flags ->
-  evar_map -> env -> ltac_var_map ->
+  env -> evar_map -> ltac_var_map ->
   typing_constraint -> glob_constr -> pure_open_constr
 
 (** Standard call to get a constr from a glob_constr, resolving implicit args *)
 
 val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
-  evar_map -> env -> glob_constr -> constr Evd.in_evar_universe_context
+  env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context
 
 (** Idem but returns the judgment of the understood term *)
 
-val understand_judgment : evar_map -> env -> 
+val understand_judgment : env -> evar_map -> 
   glob_constr -> unsafe_judgment Evd.in_evar_universe_context
 
 (** Idem but do not fail on unresolved evars *)
-val understand_judgment_tcc : evar_map ref -> env -> 
+val understand_judgment_tcc : env -> evar_map ref ->
   glob_constr -> unsafe_judgment
 
 (** Trying to solve remaining evars and remaining conversion problems
@@ -128,7 +128,7 @@ val pretype_type :
   ltac_var_map -> glob_constr -> unsafe_type_judgment
 
 val ise_pretype_gen :
-  inference_flags -> evar_map -> env ->
+  inference_flags -> env -> evar_map ->
   ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr
 
 (**/**)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 91447573f..acae69b68 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -104,7 +104,7 @@ let destEvalRefU c = match kind_of_term c with
   | Evar ev -> (EvalEvar ev, Univ.Instance.empty)
   | _ -> anomaly (Pp.str "Not an unfoldable reference")
 
-let unsafe_reference_opt_value sigma env eval = 
+let unsafe_reference_opt_value env sigma eval = 
   match eval with
   | EvalConst cst ->
     (match (lookup_constant cst env).Declarations.const_body with 
@@ -118,7 +118,7 @@ let unsafe_reference_opt_value sigma env eval =
       Option.map (lift n) v
   | EvalEvar ev -> Evd.existential_opt_value sigma ev
 
-let reference_opt_value sigma env eval u = 
+let reference_opt_value env sigma eval u = 
   match eval with
   | EvalConst cst -> constant_opt_value_in env (cst,u)
   | EvalVar id ->
@@ -130,8 +130,8 @@ let reference_opt_value sigma env eval u =
   | EvalEvar ev -> Evd.existential_opt_value sigma ev
 
 exception NotEvaluable
-let reference_value sigma env c u =
-  match reference_opt_value sigma env c u with
+let reference_value env sigma c u =
+  match reference_opt_value env sigma c u with
     | None -> raise NotEvaluable
     | Some d -> d
 
@@ -235,7 +235,7 @@ let invert_name labs l na0 env sigma ref = function
 	match refi with
 	  | None -> None
 	  | Some ref ->
-	      try match unsafe_reference_opt_value sigma env ref with
+	      try match unsafe_reference_opt_value env sigma ref with
 		| None -> None
 		| Some c ->
 		    let labs',ccl = decompose_lam c in
@@ -253,7 +253,7 @@ let invert_name labs l na0 env sigma ref = function
    [compute_consteval_mutual_fix] only one by one, until finding the
    last one before the Fix if the latter is mutually defined *)
 
-let compute_consteval_direct sigma env ref =
+let compute_consteval_direct env sigma ref =
   let rec srec env n labs onlyproj c =
     let c',l = whd_betadelta_stack env sigma c in
     match kind_of_term c' with
@@ -267,11 +267,11 @@ let compute_consteval_direct sigma env ref =
       | Proj (p, d) when isRel d -> EliminationProj n
       | _ -> NotAnElimination
   in
-  match unsafe_reference_opt_value sigma env ref with
+  match unsafe_reference_opt_value env sigma ref with
     | None -> NotAnElimination
     | Some c -> srec env 0 [] false c
 
-let compute_consteval_mutual_fix sigma env ref =
+let compute_consteval_mutual_fix env sigma ref =
   let rec srec env minarg labs ref c =
     let c',l = whd_betalet_stack sigma c in
     let nargs = List.length l in
@@ -280,7 +280,7 @@ let compute_consteval_mutual_fix sigma env ref =
 	  srec (push_rel (na,None,t) env) (minarg+1) (t::labs) ref g
       | Fix ((lv,i),(names,_,_)) ->
 	  (* Last known constant wrapping Fix is ref = [labs](Fix l) *)
-	  (match compute_consteval_direct sigma env ref with
+	  (match compute_consteval_direct env sigma ref with
 	     | NotAnElimination -> (*Above const was eliminable but this not!*)
 		 NotAnElimination
 	     | EliminationFix (minarg',minfxargs,infos) ->
@@ -293,31 +293,31 @@ let compute_consteval_mutual_fix sigma env ref =
       | _ when isEvalRef env c' ->
 	  (* Forget all \'s and args and do as if we had started with c' *)
 	  let ref,_ = destEvalRefU c' in
-	  (match unsafe_reference_opt_value sigma env ref with
+	  (match unsafe_reference_opt_value env sigma ref with
 	    | None -> anomaly (Pp.str "Should have been trapped by compute_direct")
 	    | Some c -> srec env (minarg-nargs) [] ref c)
       | _ -> (* Should not occur *) NotAnElimination
   in
-  match unsafe_reference_opt_value sigma env ref with
+  match unsafe_reference_opt_value env sigma ref with
     | None -> (* Should not occur *) NotAnElimination
     | Some c -> srec env 0 [] ref c
 
-let compute_consteval sigma env ref =
-  match compute_consteval_direct sigma env ref with
+let compute_consteval env sigma ref =
+  match compute_consteval_direct env sigma ref with
     | EliminationFix (_,_,(nbfix,_,_)) when not (Int.equal nbfix 1) ->
-	compute_consteval_mutual_fix sigma env ref
+	compute_consteval_mutual_fix env sigma ref
     | elim -> elim
 
-let reference_eval sigma env = function
+let reference_eval env sigma = function
   | EvalConst cst as ref ->
       (try
 	 Cmap.find cst !eval_table
        with Not_found -> begin
-	 let v = compute_consteval sigma env ref in
+	 let v = compute_consteval env sigma ref in
 	 eval_table := Cmap.add cst v !eval_table;
 	 v
        end)
-  | ref -> compute_consteval sigma env ref
+  | ref -> compute_consteval env sigma ref
 
 (* If f is bound to EliminationFix (n',infos), then n' is the minimal
    number of args for starting the reduction and infos is
@@ -385,7 +385,7 @@ let substl_with_function subst sigma constr =
     if i <= k + Array.length v then
       match v.(i-k-1) with
       | (fx, Some (min, ref)) ->
-        let (sigma, evk) = Evarutil.new_pure_evar !evd venv dummy in
+        let (sigma, evk) = Evarutil.new_pure_evar venv !evd dummy in
         evd := sigma;
         minargs := Evar.Map.add evk min !minargs;
         lift k (mkEvar (evk, [|fx;ref|]))
@@ -415,7 +415,7 @@ let solve_arity_problem env sigma fxminargs c =
           List.iter (check strict) rcargs
       | (Var _|Const _) when isEvalRef env h ->
           (let ev, u = destEvalRefU h in
-	     match reference_opt_value sigma env ev u with
+	     match reference_opt_value env sigma ev u with
              | Some h' ->
                 let bak = !evm in
                 (try List.iter (check false) rcargs
@@ -529,7 +529,7 @@ let match_eval_ref env constr =
   | Evar ev -> Some (EvalEvar ev, Univ.Instance.empty)
   | _ -> None
 
-let match_eval_ref_value sigma env constr = 
+let match_eval_ref_value env sigma constr = 
   match kind_of_term constr with
   | Const (sp, u) when is_evaluable env (EvalConstRef sp) ->
     Some (constant_value_in env (sp, u))
@@ -545,7 +545,7 @@ let special_red_case env sigma whfun (ci, p, c, lf)  =
     let (constr, cargs) = whfun s in
     match match_eval_ref env constr with
     | Some (ref, u) ->
-      (match reference_opt_value sigma env ref u with
+      (match reference_opt_value env sigma ref u with
       | None -> raise Redelimination
       | Some gvalue ->
         if reducible_mind_case gvalue then
@@ -657,20 +657,20 @@ let rec red_elim_const env sigma ref u largs =
           n >= 0 && not is_empty && nargs >= n,
 	  List.mem `ReductionDontExposeCase f
   in
-  try match reference_eval sigma env ref with
+  try match reference_eval env sigma ref with
     | EliminationCases n when nargs >= n ->
-	let c = reference_value sigma env ref u in
+	let c = reference_value env sigma ref u in
 	let c', lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
 	let whfun = whd_simpl_stack env sigma in
         (special_red_case env sigma whfun (destCase c'), lrest), nocase
     | EliminationProj n when nargs >= n ->
-	let c = reference_value sigma env ref u in
+	let c = reference_value env sigma ref u in
 	let c', lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
 	let whfun = whd_construct_stack env sigma in
 	let whfun' = whd_simpl_stack env sigma in
 	  (reduce_proj env sigma whfun whfun' c', lrest), nocase
     | EliminationFix (min,minfxargs,infos) when nargs >= min ->
-	let c = reference_value sigma env ref u in
+	let c = reference_value env sigma ref u in
 	let d, lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
 	let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) u largs in
 	let whfun = whd_construct_stack env sigma in
@@ -679,7 +679,7 @@ let rec red_elim_const env sigma ref u largs =
            | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase)
     | EliminationMutualFix (min,refgoal,refinfos) when nargs >= min ->
 	let rec descend (ref,u) args =
-	  let c = reference_value sigma env ref u in
+	  let c = reference_value env sigma ref u in
 	  if evaluable_reference_eq ref refgoal then
 	    (c,args)
 	  else
@@ -693,11 +693,11 @@ let rec red_elim_const env sigma ref u largs =
 	   | NotReducible -> raise Redelimination
 	   | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase)
     | NotAnElimination when unfold_nonelim ->
-         let c = reference_value sigma env ref u in
+         let c = reference_value env sigma ref u in
            (whd_betaiotazeta sigma (applist (c, largs)), []), nocase
     | _ -> raise Redelimination
     with Redelimination when unfold_anyway ->
-       let c = reference_value sigma env ref u in
+       let c = reference_value env sigma ref u in
 	 (whd_betaiotazeta sigma (applist (c, largs)), []), nocase
 
 and reduce_params env sigma stack l =
@@ -786,7 +786,7 @@ and whd_construct_stack env sigma s =
   if reducible_mind_case constr then s'
   else match match_eval_ref env constr with
   | Some (ref, u) ->
-    (match reference_opt_value sigma env ref u with
+    (match reference_opt_value env sigma ref u with
     | None -> raise Redelimination
     | Some gvalue -> whd_construct_stack env sigma (applist(gvalue, cargs)))
   | _ -> raise Redelimination
@@ -839,7 +839,7 @@ let try_red_product env sigma c =
         | Some (ref, u) ->
           (* TO DO: re-fold fixpoints after expansion *)
           (* to get true one-step reductions *)
-	  (match reference_opt_value sigma env ref u with
+	  (match reference_opt_value env sigma ref u with
 	     | None -> raise Redelimination
 	     | Some c -> c)
 	| _ -> raise Redelimination)
@@ -893,7 +893,7 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c =
           (try
 	    redrec (red_elim_const env sigma ref stack)
            with Redelimination ->
-             match reference_opt_value sigma env ref with
+             match reference_opt_value env sigma ref with
 	       | Some c ->
 		   (match kind_of_term (strip_lam c) with
                      | CoFix _ | Fix _ -> s
@@ -916,7 +916,7 @@ let whd_simpl_stack =
 let whd_simpl_orelse_delta_but_fix env sigma c =
   let rec redrec s =
     let (constr, stack as s') = whd_simpl_stack env sigma s in
-    match match_eval_ref_value sigma env constr with
+    match match_eval_ref_value env sigma constr with
     | Some c ->
       (match kind_of_term (strip_lam c) with
       | CoFix _ | Fix _ -> s'
@@ -1188,7 +1188,7 @@ let one_step_reduce env sigma c =
           (try
              fst (red_elim_const env sigma ref u stack)
            with Redelimination ->
-	     match reference_opt_value sigma env ref u with
+	     match reference_opt_value env sigma ref u with
 	       | Some d -> (d, stack)
 	       | None -> raise NotStepReducible)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 63c30eb35..124faf05b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -86,7 +86,7 @@ let set_occurrences_of_last_arg args =
   Some AllOccurrences :: List.tl (Array.map_to_list (fun _ -> None) args)
 
 let abstract_list_all_with_dependencies env evd typ c l =
-  let evd,ev = new_evar evd env typ in
+  let evd,ev = new_evar env evd typ in
   let evd,ev' = evar_absorb_arguments env evd (destEvar ev) l in
   let argoccs = set_occurrences_of_last_arg (snd ev') in
   let evd,b =
@@ -135,7 +135,7 @@ let pose_all_metas_as_evars env evd t =
         let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
         let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
         let src = Evd.evar_source_of_meta mv !evdref in
-        let ev = Evarutil.e_new_evar evdref env ~src ty in
+        let ev = Evarutil.e_new_evar env evdref ~src ty in
         evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref;
         ev)
   | _ ->
@@ -982,7 +982,7 @@ let applyHead env evd n c  =
       match kind_of_term (whd_betadeltaiota env evd cty) with
       | Prod (_,c1,c2) ->
         let (evd',evar) =
-	  Evarutil.new_evar evd env ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in
+	  Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in
 	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
       | _ -> error "Apply_Head_Then"
   in
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 6f607133d..612ef8d7d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -335,8 +335,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
       else
         let src = evar_source_of_meta mv clenv.evd in
         let src = adjust_meta_source clenv.evd mv src in
-	let (evd,evar) =
-	  new_evar clenv.evd (cl_env clenv) ~src ty in
+	let (evd,evar) = new_evar (cl_env clenv) clenv.evd ~src ty in
 	let clenv = clenv_assign mv evar {clenv with evd=evd} in
 	fold clenv mvs in
   fold clenv dep_mvs
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 5f97e72fa..564ea4dd8 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -50,7 +50,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       Pretyping.fail_evar = false;
       Pretyping.expand_evars = true } in
     try Pretyping.understand_ltac flags
-      sigma env ltac_var (Pretyping.OfType evi.evar_concl) rawc
+      env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
     with e when Errors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
       user_err_loc
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 0acfda3d8..a5cb2edb8 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -40,7 +40,7 @@ let init sigma =
   | (env, typ) :: l ->
     let ret, { solution = sol; comb = comb } = aux l in
     let src = (Loc.ghost,Evar_kinds.GoalEvar) in
-    let (new_defs , econstr) = Evarutil.new_evar sol env ~src typ in
+    let (new_defs , econstr) = Evarutil.new_evar env sol ~src typ in
     let (e, _) = Term.destEvar econstr in
     let gl = Goal.build e in
     let entry = (econstr, typ) :: ret in
@@ -59,7 +59,7 @@ let dependent_init =
   let rec aux = function
   | TNil sigma -> [], { solution = sigma; comb = []; }
   | TCons (env, sigma, typ, t) ->
-    let (sigma, econstr ) = Evarutil.new_evar sigma env typ in
+    let (sigma, econstr ) = Evarutil.new_evar env sigma typ in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let (e, _) = Term.destEvar econstr in
     let gl = Goal.build e in
@@ -950,7 +950,7 @@ struct
 
   let new_evar (evd, evs) env typ =
     let src = (Loc.ghost, Evar_kinds.GoalEvar) in
-    let (evd, ev) = Evarutil.new_evar evd env ~src typ in
+    let (evd, ev) = Evarutil.new_evar env evd ~src typ in
     let evd = Typeclasses.mark_unresolvables 
       ~filter:(fun ev' _ -> Evar.equal (fst (Term.destEvar ev)) ev') evd in
     let (evk, _) = Term.destEvar ev in
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index bec80f70d..36f2b14cb 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -434,8 +434,8 @@ let start_proof_com kind thms hook =
   let env0 = Global.env () in
   let evdref = ref (Evd.from_env env0) in
   let thms = List.map (fun (sopt,(bl,t,guard)) ->
-    let impls, ((env, ctx), imps) = interp_context_evars evdref env0 bl in
-    let t', imps' = interp_type_evars_impls ~impls evdref env t in
+    let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
+    let t', imps' = interp_type_evars_impls ~impls env evdref t in
     check_evars_are_solved env Evd.empty !evdref;
     let ids = List.map pi1 ctx in
       (compute_proof_name (pi1 kind) sopt,
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 67484429f..e386728fe 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -912,7 +912,7 @@ let prepare_hint check env init (sigma,c) =
 let interp_hints poly =
   fun h ->
   let f c =
-    let evd,c = Constrintern.interp_open_constr Evd.empty (Global.env()) c in
+    let evd,c = Constrintern.interp_open_constr (Global.env()) Evd.empty c in
       prepare_hint true (Global.env()) Evd.empty (evd,c) in
   let fr r =
     let gr = global_with_alias r in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 74fa77e6d..5e94f1b3b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -763,7 +763,7 @@ let injectable env sigma t1 t2 =
 
  *)
 
-(* [descend_then sigma env head dirn]
+(* [descend_then env sigma head dirn]
 
    returns the number of products introduced, and the environment
    which is active, in the body of the case-branch given by [dirn],
@@ -778,7 +778,7 @@ let injectable env sigma t1 t2 =
    the continuation then constructs the case-split.
  *)
 
-let descend_then sigma env head dirn =
+let descend_then env sigma head dirn =
   let IndType (indf,_) =
     try find_rectype env sigma (get_type_of env sigma head)
     with Not_found ->
@@ -821,7 +821,7 @@ let descend_then sigma env head dirn =
    constructs a case-split on [headval], with the [dirn]-th branch
    giving [True], and all the rest giving False. *)
 
-let construct_discriminator sigma env dirn c sort =
+let construct_discriminator env sigma dirn c sort =
   let IndType(indf,_) =
     try find_rectype env sigma (get_type_of env sigma c)
     with Not_found ->
@@ -848,12 +848,12 @@ let construct_discriminator sigma env dirn c sort =
   let ci = make_case_info env ind RegularStyle in
   mkCase (ci, p, c, Array.of_list brl)
 
-let rec build_discriminator sigma env dirn c sort = function
-  | [] -> construct_discriminator sigma env dirn c sort
+let rec build_discriminator env sigma dirn c sort = function
+  | [] -> construct_discriminator env sigma dirn c sort
   | ((sp,cnum),argnum)::l ->
-      let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
+      let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
       let newc = mkRel(cnum_nlams-argnum) in
-      let subval = build_discriminator sigma cnum_env dirn newc sort l  in
+      let subval = build_discriminator cnum_env sigma dirn newc sort l  in
       kont subval (build_coq_False (),mkSort (Prop Null))
 
 (* Note: discrimination could be more clever: if some elimination is
@@ -919,7 +919,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
   let e = next_ident_away eq_baseid (ids_of_context env) in
   let e_env = push_named (e,None,t) env in
   let discriminator =
-    build_discriminator sigma e_env dirn (mkVar e) sort cpath in
+    build_discriminator e_env sigma dirn (mkVar e) sort cpath in
   let sigma,(pf, absurd_term), eff = 
     discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in
   let pf_ty = mkArrow eqn absurd_term in
@@ -1111,7 +1111,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
 	| (_sigS,[a;p]) -> (a,p)
  	| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in
-      let ev = Evarutil.e_new_evar evdref env a in
+      let ev = Evarutil.e_new_evar env evdref a in
       let rty = beta_applist(p_i_minus_1,[ev]) in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
       match
@@ -1161,7 +1161,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 
    If [zty] has no dependencies, this is simple. Otherwise, assume
    [zty] has free (de Bruijn) variables in,...i1 then the role of
-   [make_iterated_tuple sigma env (term,typ) (z,zty)] is to build the
+   [make_iterated_tuple env sigma (term,typ) (z,zty)] is to build the
    tuple
 
    [existT [xn]Pn Rel(in) .. (existT [x2]P2 Rel(i2) (existT [x1]P1 Rel(i1) z))]
@@ -1200,19 +1200,19 @@ let make_iterated_tuple env sigma dflt (z,zty) =
   let sigma, dfltval = sig_clausal_form env sigma sort_of_zty n tuplety dflt in
     sigma, (tuple,tuplety,dfltval)
 
-let rec build_injrec sigma env dflt c = function
+let rec build_injrec env sigma dflt c = function
   | [] -> make_iterated_tuple env sigma dflt (c,type_of env sigma c)
   | ((sp,cnum),argnum)::l ->
     try
-      let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
+      let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
       let newc = mkRel(cnum_nlams-argnum) in
-      let sigma, (subval,tuplety,dfltval) = build_injrec sigma cnum_env dflt newc l in
+      let sigma, (subval,tuplety,dfltval) = build_injrec cnum_env sigma dflt newc l in
 	sigma, (kont subval (dfltval,tuplety), tuplety,dfltval)
     with
 	UserError _ -> failwith "caught"
 
-let build_injector sigma env dflt c cpath =
-  let sigma, (injcode,resty,_) = build_injrec sigma env dflt c cpath in
+let build_injector env sigma dflt c cpath =
+  let sigma, (injcode,resty,_) = build_injrec env sigma dflt c cpath in
     sigma, (injcode,resty)
 
 (*
@@ -1289,7 +1289,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
   let filter (cpath, t1', t2') =
     try
       (* arbitrarily take t1' as the injector default value *)
-      let sigma, (injbody,resty) = build_injector !evdref e_env t1' (mkVar e) cpath in
+      let sigma, (injbody,resty) = build_injector e_env !evdref t1' (mkVar e) cpath in
       let injfun = mkNamedLambda e t injbody in
       let sigma,congr = Evd.fresh_global env sigma eq.congr in
       let pf = applist(congr,[t;resty;injfun;t1;t2]) in
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 33505c7fc..7c4c9c965 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -71,7 +71,7 @@ let let_evar name typ =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
-    let sigma',evar = Evarutil.new_evar sigma env ~src typ in
+    let sigma',evar = Evarutil.new_evar env sigma ~src typ in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma'))
       (Tactics.letin_tac None name evar None Locusops.nowhere)
   end
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index f70191867..e4ba9a7ee 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -269,7 +269,7 @@ let add_rewrite_hint bases ort t lcsr =
   let env = Global.env() and sigma = Evd.empty in
   let poly = Flags.is_universe_polymorphism () in 
   let f ce = 
-    let c, ctx = Constrintern.interp_constr sigma env ce in
+    let c, ctx = Constrintern.interp_constr env sigma ce in
     let ctx =
       if poly then 
 	Evd.evar_universe_context_set ctx
@@ -372,7 +372,7 @@ let refine_tac {Glob_term.closure=closure;term=term} =
       Pretyping.ltac_uconstrs = closure.Glob_term.untyped;
       Pretyping.ltac_idents = closure.Glob_term.idents;
     } in
-    let update evd = Pretyping.understand_ltac flags evd env lvar tycon term in
+    let update evd = Pretyping.understand_ltac flags env evd lvar tycon term in
     Proofview.Refine.refine ~unsafe:false (fun h -> Proofview.Refine.update h update) <*>
     Proofview.V82.tactic (reduce refine_red_flags refine_locs)
   end
@@ -505,7 +505,7 @@ let inTransitivity : bool * constr -> obj =
 (* Main entry points *)
 
 let add_transitivity_lemma left lem =
- let lem',ctx (*FIXME*) = Constrintern.interp_constr Evd.empty (Global.env ()) lem in
+ let lem',ctx (*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty lem in
   add_anonymous_leaf (inTransitivity (left,lem'))
 
 (* Vernacular syntax *)
@@ -545,8 +545,8 @@ END
 
 VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF
  | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] ->
-           [ let tc,ctx = Constrintern.interp_constr Evd.empty (Global.env ()) c in
-             let tb,ctx(*FIXME*) = Constrintern.interp_constr Evd.empty (Global.env ()) b in
+           [ let tc,ctx = Constrintern.interp_constr (Global.env ()) Evd.empty c in
+             let tb,ctx(*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty b in
              Global.register f tc tb ]
 END
 
@@ -633,7 +633,7 @@ let hResolve id c occ t gl =
   let t_raw = Detyping.detype true env_ids env_names sigma t in
   let rec resolve_hole t_hole =
     try 
-      Pretyping.understand sigma env t_hole
+      Pretyping.understand env sigma t_hole
     with
       | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e ->
           let loc = match Loc.get_loc e with None -> Loc.ghost | Some loc -> loc in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index e9dace858..7eb81c3f4 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -237,7 +237,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
 
 let add_inversion_lemma_exn na com comsort bool tac =
   let env = Global.env () and evd = ref Evd.empty in
-  let c = Constrintern.interp_type_evars evd env com in
+  let c = Constrintern.interp_type_evars env evd com in
   let sigma, sort = Pretyping.interp_sort !evd comsort in
   try
     add_inversion_lemma na env sigma c sort bool tac
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 5b24facc3..6a1ac2706 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -106,12 +106,12 @@ let cstrevars evars = snd evars
 
 let new_cstr_evar (evd,cstrs) env t =
   let s = Typeclasses.set_resolvable Evd.Store.empty false in
-  let evd', t = Evarutil.new_evar ~store:s evd env t in
+  let evd', t = Evarutil.new_evar ~store:s env evd t in
   let ev, _ = destEvar t in
     (evd', Evar.Set.add ev cstrs), t
 
 (** Building or looking up instances. *)
-let e_new_cstr_evar evars env t =
+let e_new_cstr_evar env evars t =
   let evd', t = new_cstr_evar !evars env t in evars := evd'; t
 
 (** Building or looking up instances. *)
@@ -364,7 +364,7 @@ end) = struct
 	  (try
 	   let params, args = Array.chop (Array.length args - 2) args in
 	   let env' = Environ.push_rel_context rels env in
-	   let evars, (evar, _) = Evarutil.new_type_evar Evd.univ_flexible sigma env' in
+	   let evars, (evar, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in
 	   let evars, inst = 
 	     app_poly env (evars,Evar.Set.empty)
 	       rewrite_relation_class [| evar; mkApp (c, params) |] in
@@ -424,7 +424,7 @@ module TypeGlobal = struct
 
 
   let inverse env (evd,cstrs) car rel = 
-    let evd, (sort,_) = Evarutil.new_type_evar Evd.univ_flexible evd env in
+    let evd, (sort,_) = Evarutil.new_type_evar env evd Evd.univ_flexible in
       app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |]
 
 end
@@ -1334,7 +1334,7 @@ module Strategies =
     let fold_glob c : 'a pure_strategy =
       fun state env avoid t ty cstr evars ->
 (* 	let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
-	let sigma, c = Pretyping.understand_tcc (goalevars evars) env c in
+	let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
 	let unfolded =
 	  try Tacred.try_red_product env sigma c
 	  with e when Errors.noncritical e ->
@@ -1595,13 +1595,13 @@ let cl_rewrite_clause l left2right occs clause gl =
     cl_rewrite_clause_strat strat clause gl
 
 let apply_glob_constr c l2r occs = fun () env avoid t ty cstr evars ->
-  let evd, c = (Pretyping.understand_tcc (goalevars evars) env c) in
+  let evd, c = (Pretyping.understand_tcc env (goalevars evars) c) in
     apply_lemma l2r (general_rewrite_unif_flags ()) (Evd.empty, (c, NoBindings)) 
       None occs () env avoid t ty cstr (evd, cstrevars evars)
 
 let interp_glob_constr_list env sigma =
   List.map (fun c -> 
-	      let evd, c = Pretyping.understand_tcc sigma env c in
+	      let evd, c = Pretyping.understand_tcc env sigma c in
 		(evd, (c, NoBindings)), true, None)
 
 (* Syntax for rewriting with strategies *)
@@ -1792,7 +1792,7 @@ let declare_projection n instance_id r =
 
 let build_morphism_signature m =
   let env = Global.env () in
-  let m,ctx = Constrintern.interp_constr Evd.empty env m in
+  let m,ctx = Constrintern.interp_constr env Evd.empty m in
   let sigma = Evd.from_env ~ctx env in
   let t = Typing.type_of env sigma m in
   let cstrs =
@@ -1810,7 +1810,7 @@ let build_morphism_signature m =
     (fun (ty, rel) ->
       Option.iter (fun rel ->
 	let default = e_app_poly env evd PropGlobal.default_relation [| ty; rel |] in
-	  ignore(e_new_cstr_evar evd env default))
+	  ignore(e_new_cstr_evar env evd default))
 	rel)
     cstrs
   in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a243667a5..9d2f8c904 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -512,7 +512,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   let trace =
     push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in
   let (evd,c) =
-    catch_error trace (understand_ltac flags sigma env vars kind) c
+    catch_error trace (understand_ltac flags env sigma vars kind) c
   in
   (* spiwack: to avoid unnecessary modifications of tacinterp, as this
      function already use effect, I call [run] hoping it doesn't mess
@@ -622,8 +622,8 @@ let interp_unfold ist env sigma (occs,qid) =
 let interp_flag ist env sigma red =
   { red with rConst = List.map (interp_evaluable ist env sigma) red.rConst }
 
-let interp_constr_with_occurrences ist sigma env (occs,c) =
-  let (sigma,c_interp) = interp_constr ist sigma env c in
+let interp_constr_with_occurrences ist env sigma (occs,c) =
+  let (sigma,c_interp) = interp_constr ist env sigma c in
   sigma , (interp_occurrences ist occs, c_interp)
 
 let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, c) =
@@ -1323,7 +1323,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
           Pretyping.ltac_genargs = ist.lfun;
         } in
         let (sigma,c_interp) =
-          Pretyping.understand_ltac constr_flags sigma env vars WithoutTypeConstraint term
+          Pretyping.understand_ltac constr_flags env sigma vars WithoutTypeConstraint term
         in
         Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return (Value.of_constr c_interp))
       end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d24645968..48bfeb86e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1449,7 +1449,7 @@ let vm_cast_no_check c gl =
 
 
 let exact_proof c gl =
-  let c,ctx = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl)
+  let c,ctx = Constrintern.interp_casted_constr (pf_env gl) (project gl) c (pf_concl gl)
   in tclTHEN (tclEVARUNIVCONTEXT ctx) (refine_no_check c) gl
 
 let assumption =
@@ -3021,7 +3021,7 @@ let specialize_eqs id gl =
 	| _ ->
 	    if in_eqs then acc, in_eqs, ctx, ty
 	    else
-	      let e = e_new_evar evars (push_rel_context ctx env) t in
+	      let e = e_new_evar (push_rel_context ctx env) evars t in
 		aux false ((na, Some e, t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
     | t -> acc, in_eqs, ctx, ty
   in
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index e8e3ef27d..3c29c5fcb 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 df07026f6..74122d104 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 2c8fa52b9..ebaa6a911 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 33a78110c..97f7ace0d 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 c8054cf43..c167f9b79 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 =