From 4564079be1b9e3ecdbe988e726d8e77d3059d02e Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 11 Aug 2009 09:02:16 +0000 Subject: Relatively ad hoc fix to an ill-typed instantiation bug in type inference (see file failure/evar1.v) + fix of some CUMUL problems that were in the wrong direction. We assume for the fix that ill-typed unification problems come from subtyping where we don't know yet if a coercion has to be inserted or not, and hence are of the CUMUL form. More on suspending problems of the form ?n <= Type or Prop <= ?n has to be done yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12268 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/unification.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/unification.ml') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index d48c002e2..92c176593 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -600,7 +600,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 evd (mkEvar ev,rhs); let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in if not b then error "Cannot solve unification constraints"; -- cgit v1.2.3