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.
---
 kernel/type_errors.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'kernel/type_errors.ml')

diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 9813fc566e..3a1f2ae00b 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Environ
 open Reduction
 
@@ -45,8 +45,8 @@ type ('constr, 'types) ptype_error =
   | NotAType of ('constr, 'types) punsafe_judgment
   | BadAssumption of ('constr, 'types) punsafe_judgment
   | ReferenceVariables of Id.t * 'constr
-  | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment
-      * (sorts_family * sorts_family * arity_error) option
+  | ElimArity of pinductive * Sorts.family list * 'constr * ('constr, 'types) punsafe_judgment
+      * (Sorts.family * Sorts.family * arity_error) option
   | CaseNotInductive of ('constr, 'types) punsafe_judgment
   | WrongCaseInfo of pinductive * case_info
   | NumberBranches of ('constr, 'types) punsafe_judgment * int
@@ -115,6 +115,7 @@ let error_ill_typed_rec_body env i lna vdefj vargs =
   raise (TypeError (env, IllTypedRecBody (i,lna,vdefj,vargs)))
 
 let error_elim_explain kp ki =
+  let open Sorts in
   match kp,ki with
   | (InType | InSet), InProp -> NonInformativeToInformative
   | InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *)
-- 
cgit v1.2.3