From 88afd8a9853c772b6b1681c7ae208e55e7daacbe Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 19 Nov 2017 08:11:07 +0100
Subject: [api] Deprecate Term destructors, move to Constr

We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.

This is a step towards having a single module for `Constr`.
---
 plugins/funind/indfun.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/funind/indfun.ml')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f01b6669d7..9e22ad3063 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,7 +1,8 @@
 open CErrors
+open Sorts
 open Util
 open Names
-open Term
+open Constr
 open EConstr
 open Pp
 open Indfun_common
-- 
cgit v1.2.3