diff options
Diffstat (limited to 'plugins/ssr/ssrvernac.ml4')
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 507b4631b..36dce37ae 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -9,7 +9,8 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) open Names -open Term +module CoqConstr = Constr +open CoqConstr open Termops open Constrexpr open Constrexpr_ops @@ -364,7 +365,7 @@ let coerce_search_pattern_to_sort hpat = let interp_head_pat hpat = let filter_head, p = coerce_search_pattern_to_sort hpat in - let rec loop c = match kind_of_term c with + let rec loop c = match CoqConstr.kind c with | Cast (c', _, _) -> loop c' | Prod (_, _, c') -> loop c' | LetIn (_, _, _, c') -> loop c' |