Mise en place d'un système optionnel de discharge immédiat; prise en compte des défs locales dans les arguments des inductifs; nettoyage divers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 33 insertions, 9 deletions

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 47d98e6088..e7504bf166 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -42,17 +42,16 @@ val mis_typepath : inductive_instance -> section_path
 val mis_is_recursive_subset : int list -> inductive_instance -> bool
 val mis_is_recursive : inductive_instance -> bool
 val mis_consnames : inductive_instance -> identifier array
+val mis_conspaths : inductive_instance -> section_path array
 val mis_inductive : inductive_instance -> inductive
-val mis_nf_arity : inductive_instance -> types
-val mis_user_arity : inductive_instance -> types
+val mis_arity : inductive_instance -> types
 val mis_params_ctxt : inductive_instance -> rel_context
 val mis_sort : inductive_instance -> sorts
-val mis_type_mconstruct : int -> inductive_instance -> types
+val mis_constructor_type : int -> inductive_instance -> types
 val mis_finite : inductive_instance -> bool 
 
 (* The ccl of constructor is pre-normalised in the following functions *)
 val mis_nf_lc : inductive_instance -> constr array
-val mis_type_mconstructs : inductive_instance -> constr array * constr array
 
 (*s [inductive_family] = [inductive_instance] applied to global parameters *)
 type inductive_family = IndFamily of inductive_instance * constr list
@@ -117,6 +116,16 @@ val build_dependent_constructor : constructor_summary -> constr
    the constructor argument of a dependent predicate in a cases branch *)
 val build_dependent_inductive : inductive_family -> constr
 
+(*s [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *)
+(* (this is iota operator in C. Paulin habilitation thesis) *)
+val rel_vect : int -> int -> constr array
+val rel_list : int -> int -> constr list
+
+(*s [extended_rel_vect n hyps] and [extended_rel_list n hyps]
+    generalizes [rel_vect] when local definitions may occur in parameters *)
+val extended_rel_vect : int -> rel_context -> constr array
+val extended_rel_list : int -> rel_context -> constr list
+
 (* if the arity for some inductive family [indf] associated to [(I
    params)] is [(x1:A1)...(xn:An)sort'] then [make_arity env sigma dep
    indf k] builds [(x1:A1)...(xn:An)sort] which is the arity of an
@@ -157,6 +166,14 @@ val lookup_mind_specif : inductive -> env -> inductive_instance
 
 val find_rectype : env -> 'a evar_map -> constr -> inductive_type
 
+(* [get_constructors_types indf] returns the array of the types of
+   constructors of the inductive\_family [indf], i.e. the types are
+   instantiated by the parameters of the family (the type may be not
+   in canonical form -- e.g. cf sets library) *)
+
+val get_constructors_types : inductive_family -> types array
+val get_constructor_type : inductive_family -> int -> types
+
 (* [get_constructors indf] build an array of [constructor_summary]
    from some inductive type already analysed as an [inductive_family];
    global parameters are already instanciated in the constructor
@@ -165,17 +182,24 @@ val find_rectype : env -> 'a evar_map -> constr -> inductive_type
    are not renamed when [Anonymous] *)
 
 val get_constructors : inductive_family -> constructor_summary array
-
 val get_constructor : inductive_family -> int -> constructor_summary
 
-(* [get_arity indf] returns the product and the sort of the arity of
-   the inductive family described by [indf]; global parameters are
-   already instanciated; the products signature is relative to the
+(* [get_arity_type indf] returns the type of the arity of the
+   inductive family described by [indf]; global parameters are already
+   instanciated (but the type may be not in canonical form -- e.g. cf
+   sets library); the products signature is relative to the
    environment definition of [indf]; the names of the products of the
-   constructors types are not renamed when [Anonymous] *)
+   constructors types are not renamed when [Anonymous]; [get_arity
+   indf] does the same but normalises and decomposes it as an arity *)
 
+val get_arity_type : inductive_family -> types
 val get_arity : inductive_family -> arity
 
+(* [get_arity_type indf] returns the type of the arity of the inductive
+   family described by [indf]; global parameters are already instanciated *)
+
+
+
 (* Examples: assume
   
 \begin{verbatim}