diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:17 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:17 +0200 |
| commit | 2dad86a4e71bae9905b39970384328316e53eb42 (patch) | |
| tree | 9fe7df673a3e36cfbee14f2a4afe5b5b6fc72e80 /pretyping/unification.ml | |
| parent | 257f04de91e394cea67254da547fc1b90fa6978d (diff) | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Merge commit 'upstream/8.2pl2+dfsg'
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index bfd601e2..c92f1fc6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: unification.ml 12163 2009-06-06 17:36:47Z herbelin $ *) +(* $Id: unification.ml 12268 2009-08-11 09:02:16Z herbelin $ *) open Pp open Util @@ -517,7 +517,7 @@ let order_metas metas = (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *) let solve_simple_evar_eqn env evd ev rhs = - let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (CONV,ev,rhs) in + let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (None,ev,rhs) in if not b then error_cannot_unify env (evars_of evd) (mkEvar ev,rhs); let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in if not b then error "Cannot solve unification constraints"; |