diff options
Diffstat (limited to 'parsing/search.ml')
| -rw-r--r-- | parsing/search.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/parsing/search.ml b/parsing/search.ml index fc5792fa0..5e2fc7f2c 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -20,6 +20,7 @@ open Declare open Coqast open Environ open Pattern +open Matching open Printer open Libnames open Nametab @@ -131,9 +132,9 @@ let mk_rewrite_pattern2 eq pattern = let pattern_filter pat _ a c = try try - Pattern.is_matching pat (head c) + is_matching pat (head c) with _ -> - Pattern.is_matching + is_matching pat (head (Typing.type_of (Global.env()) Evd.empty c)) with UserError _ -> false |