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/funind/recdef.mli | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'plugins/funind/recdef.mli')

diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 63bbdbe7e3..50b84731b5 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -1,3 +1,4 @@
+open Constr
 
 (* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *)
 val tclUSER_if_not_mes : 
@@ -11,9 +12,9 @@ bool ->
            Constrintern.internalization_env ->
            Constrexpr.constr_expr ->
            Constrexpr.constr_expr ->
-           int -> Constrexpr.constr_expr -> (Term.pconstant ->
+           int -> Constrexpr.constr_expr -> (pconstant ->
             Indfun_common.tcc_lemma_value ref ->
-            Term.pconstant ->
-            Term.pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit
+            pconstant ->
+            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit
 
 
-- 
cgit v1.2.3