Uniformisation of the order of arguments env and sigma.

8 files changed, 40 insertions, 40 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 67484429f2..e386728fe7 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 74fa77e6d2..5e94f1b3b0 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 33505c7fcf..7c4c9c9657 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 f701918670..e4ba9a7ee5 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 e9dace8581..7eb81c3f48 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 5b24facc34..6a1ac2706f 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 a243667a5a..9d2f8c9048 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 d24645968a..48bfeb86e4 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