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, 6 insertions, 6 deletions

diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 85b55f36c..96bda6ecc 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -75,10 +75,10 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
  	  (Pfedit.get_all_proof_names ())
   in
   let evm, c, typ, imps =
-    Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None
+    Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr t bl) None
   in
   let c = solve_tccs_in_type env id isevars evm c typ in
-    Command.start_proof id kind c (fun loc gr ->
+    Lemmas.start_proof id kind c (fun loc gr ->
       Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true imps;
       hook loc gr)
 
@@ -93,14 +93,14 @@ let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("An
 let assumption_message id =
   Flags.if_verbose message ((string_of_id id) ^ " is assumed")
 
-let declare_assumption env isevars idl is_coe k bl c nl =
+let declare_assumptions env isevars idl is_coe k bl c nl =
   if not (Pfedit.refining ()) then
     let id = snd (List.hd idl) in
     let evm, c, typ, imps =
-      Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None
+      Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr c bl) None
     in
     let c = solve_tccs_in_type env id isevars evm c typ in
-      List.iter (Command.declare_one_assumption is_coe k c imps false nl) idl
+      List.iter (Command.declare_assumption is_coe k c imps false nl) idl
   else
     errorlabstrm "Command.Assumption"
 	(str "Cannot declare an assumption while in proof editing mode.")
@@ -119,7 +119,7 @@ let vernac_assumption env isevars kind l nl =
 	List.iter (fun lid ->
 	  if global then Dumpglob.dump_definition lid (not global) "ax"
 	  else dump_variable lid) idl;
-      declare_assumption env isevars idl is_coe kind [] c nl) l
+      declare_assumptions env isevars idl is_coe kind [] c nl) l
 
 let check_fresh (loc,id) =
   if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then