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

6 files changed, 46 insertions, 22 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index b6a3c985a..035bdced7 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -297,14 +297,23 @@ GEXTEND Gram
       | "-" -> false
       | -> true ]]
   ;
+  simple_fix_binder:
+    [ [ id=name -> ([id],Default Explicit,CHole (loc, None))
+      | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c) 
+    ] ]
+  ;
   fixdecl:
-    [ [ "("; id = ident; bl=LIST0 Constr.binder; ann=fixannot;
+    [ [ "("; id = ident; bl=LIST0 simple_fix_binder; ann=fixannot;
         ":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ]
   ;
   fixannot:
     [ [ "{"; IDENT "struct"; id=name; "}" -> Some id
       | -> None ] ]
   ;
+  cofixdecl:
+    [ [ "("; id = ident; bl=LIST0 simple_fix_binder; ":"; ty=lconstr; ")" ->
+        (loc,id,bl,None,ty) ] ]
+  ;
   hintbases:
     [ [ "with"; "*" -> None
       | "with"; l = LIST1 IDENT -> Some l
@@ -387,11 +396,11 @@ GEXTEND Gram
       | "fix"; n = natural -> TacFix (None,n)
       | "fix"; id = ident; n = natural -> TacFix (Some id,n)
       | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
-	  TacMutualFix (id,n,List.map mk_fix_tac fd)
+	  TacMutualFix (false,id,n,List.map mk_fix_tac fd)
       | "cofix" -> TacCofix None
       | "cofix"; id = ident -> TacCofix (Some id)
-      | "cofix"; id = ident; "with"; fd = LIST1 fixdecl ->
-	  TacMutualCofix (id,List.map mk_cofix_tac fd)
+      | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
+	  TacMutualCofix (false,id,List.map mk_cofix_tac fd)
 
       | IDENT "pose"; id = lpar_id_coloneq; b = lconstr; ")" ->
 	  TacLetTac (Names.Name id,b,nowhere)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index aea0cf27b..8285bbad3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -123,9 +123,11 @@ GEXTEND Gram
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = identref; bl = binders_let; ":";
-        c = lconstr ->
-          VernacStartTheoremProof (thm, id, (bl, c), false, no_hook)
+    [ [ thm = thm_token; id = identref; bl = binders_let; ":"; c = lconstr;
+        l = LIST0 
+          [ "with"; id = identref; bl = binders_let; ":"; c = lconstr ->
+            (Some id,(bl,c)) ] ->
+          VernacStartTheoremProof (thm,(Some id,(bl,c))::l, false, no_hook)
       | stre = assumption_token; nl = inline; bl = assum_list -> 
 	  VernacAssumption (stre, nl, bl)
       | stre = assumptions_token; nl = inline; bl = assum_list ->
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 2a46388c3..d4befac1e 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -687,11 +687,13 @@ and pr_atom1 = function
       hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings cb)
   | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c)
   | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
-  | TacMutualFix (id,n,l) ->
+  | TacMutualFix (hidden,id,n,l) ->
+      if hidden then str "idtac" (* should caught before! *) else
       hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++
              str"with " ++ prlist_with_sep spc pr_fix_tac l)
   | TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido)
-  | TacMutualCofix (id,l) ->
+  | TacMutualCofix (hidden,id,l) ->
+      if hidden then str "idtac" (* should be caught before! *) else
       hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
              str"with " ++ prlist_with_sep spc pr_cofix_tac l)
   | TacCut c -> hov 1 (str "cut" ++ pr_constrarg c)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 9fe24f4d4..57e21c2ce 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -534,12 +534,13 @@ let rec pr_vernac = function
         | None -> mt()
         | Some cc -> str" :=" ++ spc() ++ cc))
 
-  | VernacStartTheoremProof (ki,id,(bl,c),b,d) ->
-      hov 1 (pr_thm_token ki ++ spc() ++ pr_lident id ++ spc() ++
-      (match bl with
-        | [] -> mt()
-        | _ -> pr_binders bl ++ spc())
-      ++ str":" ++ pr_spc_lconstr c)
+  | VernacStartTheoremProof (ki,l,_,_) ->
+      hov 1 (pr_thm_token ki ++ spc() ++ 
+             prlist_with_sep (fun () -> str "with ") (fun (id,(bl,c)) -> hov 0
+               (pr_opt pr_lident id ++ spc() ++
+                (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
+                str":" ++ pr_spc_lconstr c)) l)
+
   | VernacEndProof Admitted -> str"Admitted"
   | VernacEndProof (Proved (opac,o)) -> (match o with
     | None -> if opac then str"Qed" else str"Defined"
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 6313a553e..a8ddfadb2 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -313,20 +313,22 @@ let rec mlexpr_of_atomic_tactic = function
       let ido = mlexpr_of_ident_option ido in
       let n = mlexpr_of_int n in
       <:expr< Tacexpr.TacFix $ido$ $n$ >>
-  | Tacexpr.TacMutualFix (id,n,l) ->
+  | Tacexpr.TacMutualFix (b,id,n,l) ->
+      let b = mlexpr_of_bool b in
       let id = mlexpr_of_ident id in
       let n = mlexpr_of_int n in
       let f =mlexpr_of_triple mlexpr_of_ident mlexpr_of_int mlexpr_of_constr in
       let l = mlexpr_of_list f l in
-      <:expr< Tacexpr.TacMutualFix $id$ $n$ $l$ >>
+      <:expr< Tacexpr.TacMutualFix $b$ $id$ $n$ $l$ >>
   | Tacexpr.TacCofix ido ->
       let ido = mlexpr_of_ident_option ido in
       <:expr< Tacexpr.TacCofix $ido$ >>
-  | Tacexpr.TacMutualCofix (id,l) ->
+  | Tacexpr.TacMutualCofix (b,id,l) ->
+      let b = mlexpr_of_bool b in
       let id = mlexpr_of_ident id in
       let f = mlexpr_of_pair mlexpr_of_ident mlexpr_of_constr in
       let l = mlexpr_of_list f l in
-      <:expr< Tacexpr.TacMutualCofix $id$ $l$ >>
+      <:expr< Tacexpr.TacMutualCofix $b$ $id$ $l$ >>
 
   | Tacexpr.TacCut c ->
       <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >>
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index 91c1bc0c4..11b755fa0 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -34,7 +34,7 @@ let pr_rule = function
   | Nested(cmpd,_) ->
       begin
 	match cmpd with 
-	    Tactic (texp,_) -> hov 0 (pr_tactic texp)
+	  | Tactic (texp,_) -> hov 0 (pr_tactic texp)
 	  | Proof_instr (_,instr) -> hov 0 (pr_proof_instr instr)
       end
   | Daimon -> str "<Daimon>"
@@ -50,6 +50,14 @@ let pr_rule_dot = function
   | r ->
       pr_rule r ++ if uses_default_tac r then str "..." else str"."
 
+let pr_rule_dot_fnl = function
+  | Nested (Tactic (TacAtom (_,(TacMutualFix (true,_,_,_)
+                              | TacMutualCofix (true,_,_))),_),_) ->
+      (* Very big hack to not display hidden tactics in "Theorem with" *)
+      (* (would not scale!) *)
+      mt ()
+  | r -> pr_rule_dot r ++ fnl ()
+
 exception Different
 
 (* We remove from the var context of env what is already in osign *)
@@ -155,7 +163,7 @@ let rec print_script nochange sigma pf =
            (print_script nochange sigma) spfl )
     | Some(rule,spfl) ->
 	((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
-	   pr_rule_dot rule ++ fnl () ++
+	   pr_rule_dot_fnl rule ++
 	   prlist_with_sep pr_fnl
            (print_script nochange sigma) spfl )	
 
@@ -189,7 +197,7 @@ let print_treescript nochange sigma pf =
     | Some(r,spfl) ->
         let indent = if List.length spfl >= 2 then 1 else 0 in
         (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++
-        hv indent (pr_rule_dot r ++ fnl () ++ prlist_with_sep fnl aux spfl)
+        hv indent (pr_rule_dot_fnl r ++ prlist_with_sep fnl aux spfl)
   in hov 0 (aux pf)
 
 let rec print_info_script sigma osign pf =