From bfc3e8cddd58cadc1bc907914a2ccd660be53912 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 11 Oct 2011 19:18:02 +0000
Subject: 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
---
 proofs/clenv.ml    | 2 +-
 proofs/clenvtac.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 6e6fff96d1..d06c6f2e6b 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -267,7 +267,7 @@ let clenv_dependent ce = clenv_dependent_gen false ce
 
 let clenv_unify ?(flags=default_unify_flags) cv_pb t1 t2 clenv =
   { clenv with
-      evd = w_unify ~flags clenv.env cv_pb t1 t2 clenv.evd }
+      evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 }
 
 let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index ec9aada73c..ff84a343bc 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -119,7 +119,7 @@ let fail_quick_unif_flags = {
 let unifyTerms ?(flags=fail_quick_unif_flags) m n gls =
   let env = pf_env gls in
   let evd = create_goal_evar_defs (project gls) in
-  let evd' = w_unify env CONV ~flags m n evd in
+  let evd' = w_unify env evd CONV ~flags m n in
   tclIDTAC {it = gls.it; sigma =  evd'}
 
 let unify ?(flags=fail_quick_unif_flags) m gls =
-- 
cgit v1.2.3