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, 15 insertions, 9 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 895fa613fe..558ca6c218 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -1141,7 +1141,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	    then
 	      (* observe_tac ("h_fix") *) (h_fix (Some this_fix_info.name) (this_fix_info.idx +1))
 	    else
-	      h_mutual_fix this_fix_info.name (this_fix_info.idx + 1)
+	      h_mutual_fix false this_fix_info.name (this_fix_info.idx + 1)
 		other_fix_infos
 	| _ -> anomaly "Not a valid information"
     in
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 31465a7a79..82277be4df 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -947,18 +947,22 @@ and xlate_tac =
 	xlate_error "TODO: injection as"
     | TacFix (idopt, n) ->
      CT_fixtactic (xlate_ident_opt idopt, CT_int n, CT_fix_tac_list [])
-    | TacMutualFix (id, n, fixtac_list) ->
+    | TacMutualFix (false, id, n, fixtac_list) ->
      let f (id,n,c) = CT_fixtac (xlate_ident id, CT_int n, xlate_formula c) in
      CT_fixtactic
       (ctf_ID_OPT_SOME (xlate_ident id), CT_int n,
       CT_fix_tac_list (List.map f fixtac_list))
+    | TacMutualFix (true, id, n, fixtac_list) ->
+        xlate_error "TODO: non user-visible fix"
     | TacCofix idopt ->
        CT_cofixtactic (xlate_ident_opt idopt, CT_cofix_tac_list [])
-    | TacMutualCofix (id, cofixtac_list) ->
+    | TacMutualCofix (false, id, cofixtac_list) ->
      let f (id,c) = CT_cofixtac (xlate_ident id, xlate_formula c) in
      CT_cofixtactic
       (CT_coerce_ID_to_ID_OPT (xlate_ident id),
       CT_cofix_tac_list (List.map f cofixtac_list))
+    | TacMutualCofix (true, id, cofixtac_list) ->
+        xlate_error "TODO: non user-visible cofix"
     | TacIntrosUntil (NamedHyp id) -> 
 	CT_intros_until (CT_coerce_ID_to_ID_OR_INT (xlate_ident id))
     | TacIntrosUntil (AnonHyp n) -> 
@@ -1880,10 +1884,12 @@ let rec xlate_vernac =
   | VernacBeginSection (_,id) ->
       CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
   | VernacEndSegment (_,id) -> CT_section_end (xlate_ident id)
-  | VernacStartTheoremProof (k, (_,s), (bl,c), _, _) ->
+  | VernacStartTheoremProof (k, [Some (_,s), (bl,c)], _, _) ->
       CT_coerce_THEOREM_GOAL_to_COMMAND(
 	CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,
            xlate_binder_list bl, xlate_formula c))
+  | VernacStartTheoremProof _ ->
+      xlate_error "TODO: Mutually dependent theorems"
   | VernacSuspend -> CT_suspend
   | VernacResume idopt -> CT_resume (xlate_ident_opt (Option.map snd idopt))
   | VernacDefinition (k,(_,s),ProveBody (bl,typ),_) ->
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 1cfe69aa95..9641794bea 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -67,10 +67,10 @@ let solve_tccs_in_type env id isevars evm c typ =
 
 let start_proof_com env isevars sopt kind (bl,t) hook =
   let id = match sopt with
-    | Some id ->
+    | Some (loc,id) ->
         (* We check existence here: it's a bit late at Qed time *)
         if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
-          errorlabstrm "start_proof" (pr_id id ++ str " already exists");
+          user_err_loc (loc,"start_proof",pr_id id ++ str " already exists");
         id
     | None ->
 	next_global_ident_away false (id_of_string "Unnamed_thm")
@@ -117,13 +117,13 @@ let subtac (loc, command) =
   let isevars = ref (create_evar_defs Evd.empty) in
   try
   match command with
-	VernacDefinition (defkind, (locid, id), expr, hook) -> 
+	VernacDefinition (defkind, (_, id as lid), expr, hook) -> 
 	    (match expr with
 	      | ProveBody (bl, t) -> 
 		  if Lib.is_modtype () then
 		    errorlabstrm "Subtac_command.StartProof"
 		      (str "Proof editing mode not supported in module types");
-		  start_proof_and_print env isevars (Some id) (Global, DefinitionBody Definition) (bl,t) 
+		  start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) 
 		    (fun _ _ -> ())
 	      | DefineBody (bl, _, c, tycon) -> 
 		   ignore(Subtac_pretyping.subtac_proof env isevars id bl c tycon))
@@ -131,7 +131,7 @@ let subtac (loc, command) =
 	  let _ = trace (str "Building fixpoint") in
 	    ignore(Subtac_command.build_recursive l b)
 
-      | VernacStartTheoremProof (thkind, (locid, id), (bl, t), lettop, hook) ->
+      | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) ->
 	  if not(Pfedit.refining ()) then
 	    if lettop then
 	      errorlabstrm "Subtac_command.StartProof"