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

2 files changed, 33 insertions, 0 deletions

diff --git a/dev/base_include b/dev/base_include
index b6c2e4d08f..41d1ac3bbc 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -53,6 +53,7 @@
 open Names
 open Term
 open Typeops
+open Term_typing
 open Univ
 open Inductive
 open Indtypes
@@ -139,10 +140,14 @@ open Refine
 open Tacinterp
 open Tacticals
 open Tactics
+open Eqschemes
 
 open Cerrors
 open Class
 open Command
+open Indschemes
+open Ind_tables
+open Lemmas
 open Coqinit
 open Coqtop
 open Discharge
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index ebbcb46ce9..505141dd66 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,34 @@
 = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
 =========================================
 
+** Cleaning in commmand.ml
+
+Functions about starting/ending a lemma are in lemmas.ml
+Functions about inductive schemes are in indschemes.ml
+
+Functions renamed:
+
+declare_one_assumption -> declare_assumption
+declare_assumption -> declare_assumptions
+Command.syntax_definition -> Metasyntax.add_syntactic_definition
+declare_interning_data merged with add_notation_interpretation
+compute_interning_datas -> compute_full_internalization_env
+implicits_env -> internalization_env
+full_implicits_env -> full_internalization_env
+build_mutual -> do_mutual_inductive
+build_recursive -> do_fixpoint
+build_corecursive -> do_cofixpoint
+build_induction_scheme -> build_mutual_induction_scheme
+build_indrec -> build_induction_scheme
+instantiate_type_indrec_scheme -> weaken_sort_scheme
+instantiate_indrec_scheme -> modify_sort_scheme
+make_case_dep, make_case_nodep -> build_case_analysis_scheme
+make_case_gen -> build_case_analysis_scheme_default
+
+Types:
+
+decl_notation -> decl_notation option
+
 ** Cleaning in libnames/nametab interfaces
 
 Functions: