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.
---
 pretyping/inductiveops.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index b31ee03d8c..34df7d3d72 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -11,6 +11,7 @@ open Util
 open Names
 open Univ
 open Term
+open Constr
 open Vars
 open Termops
 open Declarations
@@ -643,7 +644,7 @@ let type_of_projection_knowing_arg env sigma p c ty =
    syntactic conditions *)
 
 let control_only_guard env c =
-  let check_fix_cofix e c = match kind_of_term c with
+  let check_fix_cofix e c = match kind c with
     | CoFix (_,(_,_,_) as cofix) ->
       Inductive.check_cofix e cofix
     | Fix (_,(_,_,_) as fix) ->
@@ -659,7 +660,7 @@ let control_only_guard env c =
 (* inference of subtyping condition for inductive types *)
 
 let infer_inductive_subtyping_arity_constructor
-    (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity (params : Context.Rel.t) =
+    (env, evd, csts) (subst : constr -> constr) (arcn : types) is_arity (params : Context.Rel.t) =
   let numchecked = ref 0 in
   let numparams = Context.Rel.nhyps params in
   let update_contexts (env, evd, csts) csts' =
-- 
cgit v1.2.3