- Fix bug in unification, not only named metas are turned into evars (e.g. in Ssreflect).

- Fix is_applied_rewrite_relation to look for propositional relations.

2 files changed, 22 insertions, 19 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 236dc9876..58296002f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -126,7 +126,7 @@ let rec subst_meta_instances bl c =
 
 let evar_source_of_meta mv evd =
   match Evd.meta_name evd mv with
-  | Anonymous -> assert false (* only dependent metas posed as evars (?) *)
+  | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar)
   | Name id -> (Loc.ghost,Evar_kinds.VarInstance id)
 
 let pose_all_metas_as_evars env evd t =
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 477e5bcda..d7091b5d0 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -352,6 +352,26 @@ end) = struct
     | None -> None
     | Some codom -> Some (decomp_pointwise 1 codom)
 
+  (** Looking up declared rewrite relations (instances of [RewriteRelation]) *)
+  let is_applied_rewrite_relation env sigma rels t =
+    match kind_of_term t with
+    | App (c, args) when Array.length args >= 2 ->
+      let head = if isApp c then fst (destApp c) else c in
+	if Globnames.is_global (coq_eq_ref ()) head then None
+	else
+	  (try
+	   let params, args = Array.chop (Array.length args - 2) args in
+	   let env' = Environ.push_rel_context rels env in
+	   let evars, (evar, _) = Evarutil.new_type_evar Evd.univ_flexible sigma env' in
+	   let evars, inst = 
+	     app_poly env (evars,Evar.Set.empty)
+	       rewrite_relation_class [| evar; mkApp (c, params) |] in
+	   let _ = Typeclasses.resolve_one_typeclass env' (goalevars evars) inst in
+	     Some (it_mkProd_or_LetIn t rels)
+	   with e when Errors.noncritical e -> None)
+  | _ -> None
+
+
 end
 
 (* let my_type_of env evars c = Typing.e_type_of env evars c *)
@@ -410,24 +430,7 @@ end
 let sort_of_rel env evm rel =
   Reductionops.sort_of_arity env evm (Retyping.get_type_of env evm rel)
 
-(** Looking up declared rewrite relations (instances of [RewriteRelation]) *)
-let is_applied_rewrite_relation env sigma rels t =
-  match kind_of_term t with
-  | App (c, args) when Array.length args >= 2 ->
-      let head = if isApp c then fst (destApp c) else c in
-	if Globnames.is_global (coq_eq_ref ()) head then None
-	else
-	  (try
-	      let params, args = Array.chop (Array.length args - 2) args in
-	      let env' = Environ.push_rel_context rels env in
-	      let evars, (evar, _) = Evarutil.new_type_evar Evd.univ_flexible sigma env' in
-	      let evars, inst = 
-		app_poly_check env (evars,Evar.Set.empty)
-		  TypeGlobal.rewrite_relation_class [| evar; mkApp (c, params) |] in
-	      let _ = Typeclasses.resolve_one_typeclass env' (goalevars evars) inst in
-		Some (it_mkProd_or_LetIn t rels)
-	  with e when Errors.noncritical e -> None)
-  | _ -> None
+let is_applied_rewrite_relation = PropGlobal.is_applied_rewrite_relation
 
 (* let _ = *)
 (*   Hook.set Equality.is_applied_rewrite_relation is_applied_rewrite_relation *)