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

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 11324ede96..e8ef6dd678 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -335,3 +335,22 @@ let reset_top_of_script () =
 	 up_until_matching_rule is_proof_instr pts
 	with Not_found -> top_of_tree pts)
 
+(**********************************************************************)
+(* Shortcut to build a term using tactics *)
+
+open Decl_kinds
+
+let next = let n = ref 0 in fun () -> incr n; !n
+
+let build_by_tactic typ tac =
+  let id = id_of_string ("temporary_proof"^string_of_int (next())) in
+  let sign = Decls.clear_proofs (Global.named_context ()) in
+  start_proof id (Global,Proof Theorem) sign typ (fun _ _ -> ());
+  try
+    by tac;
+    let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
+    delete_current_proof ();
+    const.const_entry_body
+  with e ->
+    delete_current_proof ();
+    raise e
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 8dcd8edc2b..f46825b0c1 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -190,5 +190,11 @@ val traverse_prev_unproven : unit -> unit
 
 (* These two functions make it possible to implement more elaborate
    proof and goal management, as it is done, for instance in pcoq *)
+
 val traverse_to : int list -> unit
 val mutate : (pftreestate -> pftreestate) -> unit
+
+
+(* [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
+
+val build_by_tactic : types -> tactic -> constr