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, 45 insertions, 0 deletions

diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
new file mode 100644
index 000000000..bf72245d6
--- /dev/null
+++ b/tactics/eqschemes.mli
@@ -0,0 +1,45 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(* This file builds schemes relative to equality inductive types *)
+
+open Names
+open Term
+open Environ
+open Ind_tables
+
+(* Builds a left-to-right rewriting scheme for an equality type *)
+
+val rew_l2r_dep_scheme_kind : individual scheme_kind
+val rew_l2r_scheme_kind : individual scheme_kind
+val rew_l2r_forward_dep_scheme_kind : individual scheme_kind
+val rew_r2l_forward_dep_scheme_kind : individual scheme_kind
+val rew_r2l_dep_scheme_kind : individual scheme_kind
+val rew_r2l_scheme_kind : individual scheme_kind
+
+val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family -> constr
+val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family -> constr
+val build_l2r_forward_rew_scheme :
+  bool -> env -> inductive -> sorts_family -> constr
+val build_r2l_forward_rew_scheme :
+  bool -> env -> inductive -> sorts_family -> constr
+
+(* Builds a symmetry scheme for a symmetrical equality type *)
+
+val build_sym_scheme : env -> inductive -> constr
+val sym_scheme_kind : individual scheme_kind
+
+val build_sym_involutive_scheme : env -> inductive -> constr
+val sym_involutive_scheme_kind : individual scheme_kind
+
+(* Builds a congruence scheme for an equality type *)
+
+val congr_scheme_kind : individual scheme_kind
+val build_congr : env -> constr * constr -> inductive -> constr