From 109c90efd0dd2bfbeb6c29b263ccd9b2e84e5b9e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 25 Aug 2014 21:46:26 +0200
Subject: Fixing bug #3377 by giving env and sigma to constrMathching. Now it's
 possible to match on a primitive projection application c.(p) using "?f _",
 binding f to (fun x => x.(p)) with the correct typing.

---
 toplevel/search.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/search.ml b/toplevel/search.ml
index e2a4ad25cf..6a7d2c8118 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -98,7 +98,7 @@ let format_display l = prlist_with_sep fnl (fun x -> x) (List.rev l)
 (** FIXME: this is quite dummy, we may find a more efficient algorithm. *)
 let rec pattern_filter pat ref env typ =
   let typ = strip_outer_cast typ in
-  if ConstrMatching.is_matching pat typ then true
+  if ConstrMatching.is_matching env Evd.empty pat typ then true
   else match kind_of_term typ with
   | Prod (_, _, typ)
   | LetIn (_, _, _, typ) -> pattern_filter pat ref env typ
@@ -106,7 +106,7 @@ let rec pattern_filter pat ref env typ =
 
 let rec head_filter pat ref env typ =
   let typ = strip_outer_cast typ in
-  if ConstrMatching.is_matching_head pat typ then true
+  if ConstrMatching.is_matching_head env Evd.empty pat typ then true
   else match kind_of_term typ with
   | Prod (_, _, typ)
   | LetIn (_, _, _, typ) -> head_filter pat ref env typ
@@ -135,7 +135,7 @@ let name_of_reference ref = Id.to_string (basename_of_global ref)
 
 let search_about_filter query gr env typ = match query with
 | GlobSearchSubPattern pat ->
-  ConstrMatching.is_matching_appsubterm ~closed:false pat typ
+  ConstrMatching.is_matching_appsubterm ~closed:false env Evd.empty pat typ
 | GlobSearchString s ->
   String.string_contains ~where:(name_of_reference gr) ~what:s
 
@@ -274,11 +274,12 @@ let interface_search flags =
       toggle (Str.string_match regexp id 0) flag
     in
     let match_type (pat, flag) =
-      toggle (ConstrMatching.is_matching pat constr) flag
+      toggle (ConstrMatching.is_matching env Evd.empty pat constr) flag
     in
     let match_subtype (pat, flag) =
       toggle
-        (ConstrMatching.is_matching_appsubterm ~closed:false pat constr) flag
+        (ConstrMatching.is_matching_appsubterm ~closed:false 
+	   env Evd.empty pat constr) flag
     in
     let match_module (mdl, flag) =
       toggle (Libnames.is_dirpath_prefix_of mdl path) flag
-- 
cgit v1.2.3