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/functional_principles_proofs.ml | 2 +-
 plugins/funind/functional_principles_types.ml  | 3 ++-
 plugins/funind/glob_term_to_relation.ml        | 1 -
 plugins/funind/indfun.ml                       | 3 ++-
 plugins/funind/recdef.ml                       | 1 -
 5 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 29e824f441..62ca706264 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,7 +1,7 @@
 open Printer
 open CErrors
 open Util
-open Term
+open Constr
 open EConstr
 open Vars
 open Namegen
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 3899bc709c..996e2b6af0 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,7 +1,8 @@
 open Printer
 open CErrors
-open Util
 open Term
+open Sorts
+open Util
 open Constr
 open Vars
 open Namegen
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index d04b7a33d1..fa43536304 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1,7 +1,6 @@
 open Printer
 open Pp
 open Names
-open Term
 open Constr
 open Vars
 open Glob_term
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
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 04d729b10c..3089ec4708 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -9,7 +9,6 @@
 
 module CVars = Vars
 
-open Term
 open Constr
 open EConstr
 open Vars
-- 
cgit v1.2.3