diff options
Diffstat (limited to 'kernel/indtypes.mli')
-rw-r--r-- | kernel/indtypes.mli | 25 |
1 files changed, 16 insertions, 9 deletions
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 1cd0a0b0..7774e52e 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -1,18 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Names -open Univ open Term open Declarations open Environ open Entries -open Typeops (** Inductive type checking and errors *) @@ -23,11 +21,11 @@ open Typeops type inductive_error = | NonPos of env * constr * constr | NotEnoughArgs of env * constr * constr - | NotConstructor of env * identifier * constr * constr * int * int + | NotConstructor of env * Id.t * constr * constr * int * int | NonPar of env * constr * int * constr * constr - | SameNamesTypes of identifier - | SameNamesConstructors of identifier - | SameNamesOverlap of identifier list + | SameNamesTypes of Id.t + | SameNamesConstructors of Id.t + | SameNamesOverlap of Id.t list | NotAnArity of env * constr | BadEntry | LargeNonPropInductiveNotInType @@ -36,5 +34,14 @@ exception InductiveError of inductive_error (** The following function does checks on inductive declarations. *) -val check_inductive : - env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body +val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body + +(** The following enforces a system compatible with the univalent model *) + +val enforce_indices_matter : unit -> unit +val is_indices_matter : unit -> bool + +val compute_projections : pinductive -> Id.t -> Id.t -> + int -> Context.rel_context -> int array -> int array -> + Context.rel_context -> + (constant array * projection_body array) |