diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
| commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
| tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /kernel/indtypes.mli | |
| parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) | |
Imported Upstream version 8.5~beta1+dfsg
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) |