Moved to a more standard order of arguments (i.e. env followed by evar_map)

for the functions of unification.ml.

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

4 files changed, 8 insertions, 8 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 8ccf751c4e..13f8784f58 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -246,7 +246,7 @@ type hypinfo = {
 
 let evd_convertible env evd x y =
   try
-    ignore(Unification.w_unify ~flags:Unification.elim_flags env Reduction.CONV x y evd); true 
+    ignore(Unification.w_unify ~flags:Unification.elim_flags env evd Reduction.CONV x y); true 
   (* try ignore(Evarconv.the_conv_x env x y evd); true *)
   with _ -> false
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d21d3e767b..2d4268e60e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -131,8 +131,8 @@ let instantiate_lemma_all frzevars env sigma gl c ty l l2r concl =
   in
   let flags = make_flags frzevars sigma rewrite_unif_flags eqclause in
   let occs =
-    Unification.w_unify_to_subterm_all ~flags env
-      ((if l2r then c1 else c2),concl) eqclause.evd
+    Unification.w_unify_to_subterm_all ~flags env eqclause.evd
+      ((if l2r then c1 else c2),concl)
   in List.map try_occ occs
 
 let instantiate_lemma env sigma gl c ty l l2r concl =
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index c908f71885..1595ded2d7 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1021,7 +1021,7 @@ module Strategies =
 	  with _ -> error "fold: the term is not unfoldable !"
 	in
 	  try
-	    let sigma = Unification.w_unify env CONV ~flags:Unification.elim_flags unfolded t sigma in
+	    let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in
 	    let c' = Evarutil.nf_evar sigma c in
 	      Some (Some { rew_car = ty; rew_from = t; rew_to = c';
 			   rew_prf = RewCast DEFAULTcast; 
@@ -1771,13 +1771,13 @@ let unification_rewrite flags l2r c1 c2 cl car rel but gl =
       (* ~flags:(false,true) to allow to mark occurrences that must not be
          rewritten simply by replacing them with let-defined definitions
          in the context *)
-      Unification.w_unify_to_subterm ~flags:rewrite_unif_flags env ((if l2r then c1 else c2),but) cl.evd
+      Unification.w_unify_to_subterm ~flags:rewrite_unif_flags env cl.evd ((if l2r then c1 else c2),but)
     with
 	Pretype_errors.PretypeError _ ->
 	  (* ~flags:(true,true) to make Ring work (since it really
              exploits conversion) *)
 	  Unification.w_unify_to_subterm ~flags:flags
-	    env ((if l2r then c1 else c2),but) cl.evd
+	    env cl.evd ((if l2r then c1 else c2),but)
   in
   let evd' = Typeclasses.resolve_typeclasses ~fail:false env evd' in
   let cl' = {cl with evd = evd'} in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2f0eaf82e0..692622f324 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1704,7 +1704,7 @@ let default_matching_flags sigma = {
 let make_pattern_test env sigma0 (sigma,c) =
   let flags = default_matching_flags sigma0 in
   let matching_fun t =
-    try let sigma = w_unify env Reduction.CONV ~flags c t sigma in Some(sigma,t)
+    try let sigma = w_unify env sigma Reduction.CONV ~flags c t in Some(sigma,t)
     with _ -> raise NotUnifiable in
   let merge_fun c1 c2 =
     match c1, c2 with
@@ -3531,6 +3531,6 @@ let unify ?(state=full_transparent_state) x y gl =
 	modulo_delta = state;
 	modulo_conv_on_closed_terms = Some state}
     in
-    let evd = w_unify (pf_env gl) Reduction.CONV ~flags x y (project gl)
+    let evd = w_unify (pf_env gl) (project gl) Reduction.CONV ~flags x y
     in tclEVARS evd gl
   with _ -> tclFAIL 0 (str"Not unifiable") gl