From f1db73816e4bd463cc81f34ba7e35857694bfa25 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 5 Jan 2015 06:42:37 +0100
Subject: Propagating the relaxing of filtering started in 48509b6, fixed in
 3cd718c, to the case of second_order_matching.

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

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 9f0e47c6c..f541698e9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -937,7 +937,7 @@ let filter_possible_projections c ty ctxt args =
   List.map_i (fun i (id,b,_) ->
     let () = assert (i < len) in
     let a = Array.unsafe_get args i in
-    not (Option.is_empty b) ||
+    (match b with None -> false | Some c -> not (isRel c || isVar c)) ||
     a == c ||
     (* Here we make an approximation, for instance, we could also be *)
     (* interested in finding a term u convertible to c such that a occurs *)
-- 
cgit v1.2.3