From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 6 Nov 2017 23:27:09 +0100
Subject: [api] Move structures deprecated in the API to the core.

We do up to `Term` which is the main bulk of the changes.
---
 plugins/ssr/ssrequality.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins/ssr/ssrequality.ml')

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 95ca6f49ad..e82f222b9c 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -11,13 +11,14 @@
 open Ltac_plugin
 open Util
 open Names
+open Term
+open Constr
 open Vars
 open Locus
 open Printer
 open Globnames
 open Termops
 open Tacinterp
-open Term
 
 open Ssrmatching_plugin
 open Ssrmatching
@@ -316,7 +317,7 @@ let rw_progress rhs lhs ise = not (EConstr.eq_constr ise lhs (Evarutil.nf_evar i
 (* such a generic Leibnitz equation -- short of inspecting the type  *)
 (* of the elimination lemmas.                                        *)
 
-let rec strip_prod_assum c = match Term.kind_of_term c with
+let rec strip_prod_assum c = match Constr.kind c with
   | Prod (_, _, c') -> strip_prod_assum c'
   | LetIn (_, v, _, c') -> strip_prod_assum (subst1 v c)
   | Cast (c', _, _) -> strip_prod_assum c'
-- 
cgit v1.2.3