diff options
author | 2017-11-13 17:13:44 +0100 | |
---|---|---|
committer | 2017-11-13 17:13:44 +0100 | |
commit | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (patch) | |
tree | 675b02e411ff2c56a9aff39f4956a055eac254a7 /plugins/ssr/ssrvernac.ml4 | |
parent | 29a7307ea7cd36408661ba633a235793f11dca84 (diff) | |
parent | 03e21974a3e971a294533bffb81877dc1bd270b6 (diff) |
Merge PR #6098: [api] Move structures deprecated in the API to the core.
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' |