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/declarations.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'kernel/declarations.ml') diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 8b949f928..b95796fd8 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr (** This module defines the internal representation of global declarations. This includes global constants/axioms, mutual @@ -28,8 +28,8 @@ type engagement = set_predicativity *) type template_arity = { - template_param_levels : Univ.universe_level option list; - template_level : Univ.universe; + template_param_levels : Univ.Level.t option list; + template_level : Univ.Universe.t; } type ('a, 'b) declaration_arity = @@ -63,8 +63,8 @@ type constant_def = | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) type constant_universes = - | Monomorphic_const of Univ.universe_context - | Polymorphic_const of Univ.abstract_universe_context + | Monomorphic_const of Univ.UContext.t + | Polymorphic_const of Univ.AUContext.t (** The [typing_flags] are instructions to the type-checker which modify its behaviour. The typing flags used in the type-checking @@ -119,7 +119,7 @@ type record_body = (Id.t * Constant.t array * projection_body array) option type regular_inductive_arity = { mind_user_arity : types; - mind_sort : sorts; + mind_sort : Sorts.t; } type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity @@ -146,7 +146,7 @@ type one_inductive_body = { mind_nrealdecls : int; (** Length of realargs context (with let, no params) *) - mind_kelim : sorts_family list; (** List of allowed elimination sorts *) + mind_kelim : Sorts.family list; (** List of allowed elimination sorts *) mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *) @@ -168,9 +168,9 @@ type one_inductive_body = { } type abstract_inductive_universes = - | Monomorphic_ind of Univ.universe_context - | Polymorphic_ind of Univ.abstract_universe_context - | Cumulative_ind of Univ.abstract_cumulativity_info + | Monomorphic_ind of Univ.UContext.t + | Polymorphic_ind of Univ.AUContext.t + | Cumulative_ind of Univ.ACumulativityInfo.t type mutual_inductive_body = { -- cgit v1.2.3