diff options
| author | herbelin | 2011-10-11 19:18:02 +0000 |
|---|---|---|
| committer | herbelin | 2011-10-11 19:18:02 +0000 |
| commit | bfc3e8cddd58cadc1bc907914a2ccd660be53912 (patch) | |
| tree | 6bf603814e6981139d53a6388f3854189a8e7f09 /proofs | |
| parent | c1234a327b8ef2b52af1410dace719000c360f53 (diff) | |
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
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 2 |
2 files changed, 2 insertions, 2 deletions
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 = |