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`.
---
 interp/impargs.ml | 1 -
 interp/reserve.ml | 2 +-
 2 files changed, 1 insertion(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/impargs.ml b/interp/impargs.ml
index f70154e613..3105214d5e 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -10,7 +10,6 @@ open CErrors
 open Util
 open Names
 open Globnames
-open Term
 open Constr
 open Reduction
 open Declarations
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 6fd1d0b581..22c5a2f5e5 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -102,7 +102,7 @@ let declare_reserved_type idl t =
 let find_reserved_type id = Id.Map.find (root_of_id id) !reserve_table
 
 let constr_key c =
-  try RefKey (canonical_gr (global_of_constr (fst (Term.decompose_app c))))
+  try RefKey (canonical_gr (global_of_constr (fst (Constr.decompose_app c))))
   with Not_found -> Oth
 
 let revert_reserved_type t =
-- 
cgit v1.2.3