From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 kernel/inductive.mli | 51 ++++++++++++++++++++++-----------------------------
 1 file changed, 22 insertions(+), 29 deletions(-)

(limited to 'kernel/inductive.mli')

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 0dac719c..a124647c 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -1,24 +1,20 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: inductive.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Names
 open Univ
 open Term
 open Declarations
 open Environ
-(*i*)
 
-(*s Extracting an inductive type from a construction *)
+(** {6 Extracting an inductive type from a construction } *)
 
-(* [find_m*type env sigma c] coerce [c] to an recursive type (I args).
+(** [find_m*type env sigma c] coerce [c] to an recursive type (I args).
    [find_rectype], [find_inductive] and [find_coinductive]
    respectively accepts any recursive type, only an inductive type and
    only a coinductive type.
@@ -30,32 +26,33 @@ val find_coinductive : env -> types -> inductive * constr list
 
 type mind_specif = mutual_inductive_body * one_inductive_body
 
-(*s Fetching information in the environment about an inductive type.
+(** {6 ... } *)
+(** Fetching information in the environment about an inductive type.
     Raises [Not_found] if the inductive type is not found. *)
 val lookup_mind_specif : env -> inductive -> mind_specif
 
-(*s Functions to build standard types related to inductive *)
+(** {6 Functions to build standard types related to inductive } *)
 val ind_subst : mutual_inductive -> mutual_inductive_body -> constr list
 
 val type_of_inductive : env -> mind_specif -> types
 
 val elim_sorts : mind_specif -> sorts_family list
 
-(* Return type as quoted by the user *)
+(** Return type as quoted by the user *)
 val type_of_constructor : constructor -> mind_specif -> types
 
-(* Return constructor types in normal form *)
+(** Return constructor types in normal form *)
 val arities_of_constructors : inductive -> mind_specif -> types array
 
-(* Return constructor types in user form *)
+(** Return constructor types in user form *)
 val type_of_constructors : inductive -> mind_specif -> types array
 
-(* Transforms inductive specification into types (in nf) *)
+(** Transforms inductive specification into types (in nf) *)
 val arities_of_specif : mutual_inductive -> mind_specif -> types array
 
 val inductive_params : mind_specif -> int
 
-(* [type_case_branches env (I,args) (p:A) c] computes useful types
+(** [type_case_branches env (I,args) (p:A) c] computes useful types
    about the following Cases expression:
       <p>Cases (c :: (I args)) of b1..bn end
    It computes the type of every branch (pattern variables are
@@ -70,20 +67,20 @@ val build_branches_type :
   inductive -> mutual_inductive_body * one_inductive_body ->
     constr list -> constr -> types array
 
-(* Return the arity of an inductive type *)
+(** Return the arity of an inductive type *)
 val mind_arity : one_inductive_body -> rel_context * sorts_family
 
 val inductive_sort_family : one_inductive_body -> sorts_family
 
-(* Check a [case_info] actually correspond to a Case expression on the
+(** Check a [case_info] actually correspond to a Case expression on the
    given inductive type. *)
 val check_case_info : env -> inductive -> case_info -> unit
 
-(*s Guard conditions for fix and cofix-points. *)
+(** {6 Guard conditions for fix and cofix-points. } *)
 val check_fix : env -> fixpoint -> unit
 val check_cofix : env -> cofixpoint -> unit
 
-(*s Support for sort-polymorphic inductive types *)
+(** {6 Support for sort-polymorphic inductive types } *)
 
 (** The "polyprop" optional argument below allows to control
     the "Prop-polymorphism". By default, it is allowed.
@@ -102,8 +99,7 @@ val max_inductive_sort : sorts array -> universe
 val instantiate_universes : env -> rel_context ->
     polymorphic_arity -> types array -> rel_context * sorts
 
-(***************************************************************)
-(* Debug *)
+(** {6 Debug} *)
 
 type size = Large | Strict
 type subterm_spec =
@@ -112,16 +108,13 @@ type subterm_spec =
   | Not_subterm
 type guard_env =
   { env     : env;
-    (* dB of last fixpoint *)
+    (** dB of last fixpoint *)
     rel_min : int;
-    (* inductive of recarg of each fixpoint *)
-    inds    : inductive array;
-    (* the recarg information of inductive family *)
-    recvec  : wf_paths array;
-    (* dB of variables denoting subterms *)
+    (** dB of variables denoting subterms *)
     genv    : subterm_spec Lazy.t list;
   }
 
-val subterm_specif : guard_env -> constr -> subterm_spec
-val case_branches_specif : guard_env -> subterm_spec Lazy.t -> inductive ->
-  constr array -> (guard_env * constr) array
+type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t
+
+val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec
+
-- 
cgit v1.2.3