Uniformisation of the order of arguments env and sigma.

12 files changed, 88 insertions, 88 deletions

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