From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 kernel/indtypes.mli | 25 ++++++++++++++++---------
 1 file changed, 16 insertions(+), 9 deletions(-)

(limited to 'kernel/indtypes.mli')

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)
-- 
cgit v1.2.3