Restructuration of command.ml + generic infrastructure for inductive schemes

- Cleaning and uniformisation in command.ml:
  - For better modularity and better visibility, two files got isolated
    out of command.ml:
    - lemmas.ml is about starting and saving a proof
    - indschemes.ml is about declaring inductive schemes
  - Decomposition of the functions of command.ml into a functional part
    and the imperative part
- Inductive schemes:
  - New architecture in ind_tables.ml for registering scheme builders,
    and for sharing and generating on demand inductive schemes
  - Adding new automatically generated equality schemes (file eqschemes.ml)
    - "_congr" for equality types (completing here commit 12273)
    - "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep",
      "_rew_backward" (similar to eq_rect), "_rew_backward_dep" for
      rewriting schemes (warning, rew_forward_dep cannot be stated following
      the standard Coq pattern for inductive types: "t=u" cannot be the
      last argument of the scheme)
    - "_case", "_case_nodep", "_case_dep" for case analysis schemes
  - Preliminary step towards discriminate and injection working on any
    equality-like type (e.g. eq_true)
  - Restating JMeq_congr under the canonical form of congruence schemes
  - Renamed "Set Equality Scheme" into "Set Equality Schemes"
  - Added "Set Rewriting Schemes", "Set Case Analysis Schemes"
  - Activation of the automatic generation of boolean equality lemmas
  - Partial debug and error messages improvements for the generation of
    boolean equality and decidable equality
  - Added schemes for making dependent rewrite working (unfortunately with
    not a fully satisfactory design - see file eqschemes.ml)
- Some names of ML function made more regular (see dev/doc/changes.txt)
- Incidentally, added a flush to obsolete Local/Global syntax warning

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

1 files changed, 29 insertions, 25 deletions

diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index ac6a61c3c..91d559e17 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -27,36 +27,41 @@ exception RecursionSchemeError of recursion_scheme_error
 
 (** Eliminations *)
 
-(* These functions build elimination predicate for Case tactic *)
+type dep_flag = bool
 
-val make_case_dep : env -> evar_map -> inductive -> sorts_family -> constr
-val make_case_nodep : env -> evar_map -> inductive -> sorts_family -> constr
-val make_case_gen : env -> evar_map -> inductive -> sorts_family -> constr
+(* Build a case analysis elimination scheme in some sort family *)
 
-(* This builds an elimination scheme associated (using the own arity
-   of the inductive) *)
+val build_case_analysis_scheme : env -> evar_map -> inductive ->
+      dep_flag -> sorts_family -> constr
 
-val build_indrec : env -> evar_map -> inductive -> constr
-val instantiate_indrec_scheme : sorts -> int -> constr -> constr
-val instantiate_type_indrec_scheme : sorts -> int -> constr -> types ->
-  constr * types
+(* Build a dependent case elimination predicate unless type is in Prop *)
 
-(** Complex recursion schemes [Scheme] *)
+val build_case_analysis_scheme_default : env -> evar_map -> inductive ->
+      sorts_family -> constr
 
-val build_mutual_indrec :
-  env -> evar_map ->
-    (inductive * mutual_inductive_body * one_inductive_body
-    * bool * sorts_family) list
-    -> constr list
+(* Builds a recursive induction scheme (Peano-induction style) in the same
+   sort family as the inductive family; it is dependent if not in Prop *)
 
-(** Old Case/Match typing *)
+val build_induction_scheme : env -> evar_map -> inductive ->
+      dep_flag -> sorts_family -> constr
 
-val type_rec_branches : bool -> env -> evar_map -> inductive_type
-  -> constr -> constr -> constr array * constr
-val make_rec_branch_arg :
-  env -> evar_map ->
-    int * ('b * constr) option array * int ->
-    constr -> constructor_summary -> wf_paths list -> constr
+(* Builds mutual (recursive) induction schemes *)
+
+val build_mutual_induction_scheme :
+  env -> evar_map -> (inductive * dep_flag * sorts_family) list -> constr list
+
+(** Scheme combinators *)
+
+(* [modify_sort_scheme s n c] modifies the quantification sort of
+   scheme c whose predicate is abstracted at position [n] of [c] *)
+
+val modify_sort_scheme : sorts -> int -> constr -> constr
+
+(* [weaken_sort_scheme s n c t] derives by subtyping from [c:t]
+   whose conclusion is quantified on [Type] at position [n] of [t] a
+   scheme quantified on sort [s] *)
+
+val weaken_sort_scheme : sorts -> int -> constr -> types -> constr * types
 
 (** Recursor names utilities *)
 
@@ -64,5 +69,4 @@ val lookup_eliminator : inductive -> sorts_family -> constr
 val elimination_suffix : sorts_family -> string
 val make_elimination_ident : identifier -> sorts_family -> identifier
 
-
-
+val case_suffix : string