From 7273a302676a0ecb4f51d39dbe5cc8848b886473 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 4 Sep 2008 08:59:41 +0000
Subject: Fix camlp5-ism "Ploc.Exc" and add a unification fix: when solving an
 evar, do unification between the evar type and the type of the instance to
 properly propagate information. Typical example: in context ?A : Type, ?R :
 relation ?A. When we instantiate ?R using a goal like x = y by @eq t, we need
 to instantiate A to t as well.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11357 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/unification.ml  | 9 ++++++---
 tactics/class_tactics.ml4 | 2 +-
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index dbf7d6469e..a1066df7a5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -490,9 +490,12 @@ let w_merge env with_types flags (metas,evars) evd =
 	      let evd' = mimick_evar evd flags f (Array.length cl) evn in
 	      w_merge_rec evd' metas evars eqns
           | _ ->
-	      w_merge_rec (solve_simple_evar_eqn env evd ev rhs') 
-	        metas evars' eqns
-	  end
+	      let evi = Evd.find (evars_of evd) evn in
+	      let rty = Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) rhs' in
+	      let evd', rhs'' = w_coerce_to_type env evd rhs' rty evi.evar_concl in
+	      let evd'' = solve_simple_evar_eqn env evd' ev rhs'' in
+		w_merge_rec evd'' metas evars' eqns
+	end
     | [] -> 
 
     (* Process metas *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index e1395ed8b7..976974e78f 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -1718,7 +1718,7 @@ let setoid_proof gl ty ?(bindings=NoBindings) meth fallback =
       (CRef (Qualid (dummy_loc, Nametab.shortest_qualid_of_global Idset.empty
 	(Lazy.force meth)))) ~bindings gl
   with Not_found | Typeclasses_errors.TypeClassError (_, _) |
-      Ploc.Exc (_, Typeclasses_errors.TypeClassError (_, _)) -> 
+      Stdpp.Exc_located (_, Typeclasses_errors.TypeClassError (_, _)) -> 
 	match fallback gl with 
 	| Some tac -> tac gl
 	| None ->
-- 
cgit v1.2.3