Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve

des théorèmes prouvés par récursion ou corécursion mutuelle.

Correction au passage du parsing et du printing des tactiques
fix/cofix et documentation de ces tactiques.



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

3 files changed, 18 insertions, 12 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 81216d1697..6dad6471d7 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -33,6 +33,7 @@ open Safe_typing
 
 type proof_topstate = {
   mutable top_end_tac : tactic option;
+  top_init_tac : tactic option;
   top_goal : goal;
   top_strength : Decl_kinds.goal_kind;
   top_hook : declaration_hook }
@@ -118,8 +119,6 @@ let delete_proof (loc,id) =
     user_err_loc
       (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
       
-let init_proofs () = Edit.clear proof_edits
-		       
 let mutate f =
   try 
     Edit.mutate proof_edits (fun _ pfs -> f pfs)
@@ -128,7 +127,8 @@ let mutate f =
       (str"No focused proof" ++ msg_proofs true)
 
 let start (na,ts) =
-  let pfs = mk_pftreestate ts.top_goal in 
+  let pfs = mk_pftreestate ts.top_goal in
+  let pfs = Option.fold_right solve_pftreestate ts.top_init_tac pfs in
   add_proof(na,pfs,ts)
     
 let restart_proof () =
@@ -238,7 +238,7 @@ let check_no_pending_proofs () =
 
 let delete_current_proof () = delete_proof_gen (get_current_proof_name ())
 
-let delete_all_proofs = init_proofs
+let delete_all_proofs () = Edit.clear proof_edits
 
 (*********************************************************************)
 (*   Modifying the end tactic of the current profftree               *)
@@ -251,10 +251,11 @@ let set_end_tac tac =
 (*              Modifying the current prooftree                      *)
 (*********************************************************************)
 
-let start_proof na str sign concl hook =
+let start_proof na str sign concl ?init_tac hook =
   let top_goal = mk_goal sign concl None in
   let ts = { 
     top_end_tac = None;
+    top_init_tac = init_tac;
     top_goal = top_goal;
     top_strength = str;
     top_hook = hook}
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 5de956d465..ad7c5e51ab 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -71,13 +71,16 @@ val current_proof_depth: unit -> int
 val set_undo : int option -> unit
 val get_undo : unit -> int option
 
-(*s [start_proof s str env t hook] starts a proof of name [s] and conclusion
-    [t]; [hook] is optionally a function to be applied at proof end (e.g. to
-    declare the built constructions as a coercion or a setoid morphism) *)
+(*s [start_proof s str env t hook tac] starts a proof of name [s] and
+    conclusion [t]; [hook] is optionally a function to be applied at
+    proof end (e.g. to declare the built constructions as a coercion
+    or a setoid morphism); init_tac is possibly a tactic to
+    systematically apply at initialization time (e.g. to start the
+    proof of mutually dependent theorems) *)
 
 val start_proof : 
-  identifier -> goal_kind -> named_context_val -> constr
-    -> declaration_hook -> unit
+  identifier -> goal_kind -> named_context_val -> constr ->
+    ?init_tac:tactic -> declaration_hook -> unit
 
 (* [restart_proof ()] restarts the current focused proof from the beginning
    or fails if no proof is focused *)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index a13f8bf708..34699c5fdd 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -26,6 +26,7 @@ type evars_flag = bool     (* true = pose evars       false = fail on evars *)
 type rec_flag = bool       (* true = recursive        false = not recursive *)
 type advanced_flag = bool  (* true = advanced         false = basic *)
 type split_flag = bool     (* true = exists           false = split *)
+type hidden_flag = bool    (* true = internal use     false = user-level *)
 
 type raw_red_flag =
   | FBeta
@@ -140,9 +141,10 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacCase of evars_flag * 'constr with_bindings
   | TacCaseType of 'constr
   | TacFix of identifier option * int
-  | TacMutualFix of identifier * int * (identifier * int * 'constr) list
+  | TacMutualFix of hidden_flag * identifier * int * (identifier * int * 
+      'constr) list
   | TacCofix of identifier option
-  | TacMutualCofix of identifier * (identifier * 'constr) list
+  | TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list
   | TacCut of 'constr
   | TacAssert of 'tac option * intro_pattern_expr * 'constr
   | TacGeneralize of 'constr list