From 2a8e86e504e57d3c47d65fee408cec9aa9419445 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 19 Jun 2014 12:43:35 +0200
Subject: - 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.

---
 pretyping/unification.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 236dc98765..58296002f9 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 =
-- 
cgit v1.2.3