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

1 files changed, 5 insertions, 4 deletions

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 0cb314201..c3b7e0a8b 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -49,14 +49,15 @@ let h_elim_type c    = abstract_tactic (TacElimType (inj_open c)) (elim_type c)
 let h_case ev cb     = abstract_tactic (TacCase (ev,inj_open_wb cb)) (general_case_analysis ev cb)
 let h_case_type c    = abstract_tactic (TacCaseType (inj_open c)) (case_type c)
 let h_fix ido n      = abstract_tactic (TacFix (ido,n)) (fix ido n)
-let h_mutual_fix id n l =
+let h_mutual_fix b id n l =
   abstract_tactic
-    (TacMutualFix (id,n,List.map (fun (id,n,c) -> (id,n,inj_open c)) l))
+    (TacMutualFix (b,id,n,List.map (fun (id,n,c) -> (id,n,inj_open c)) l))
     (mutual_fix id n l)
+
 let h_cofix ido      = abstract_tactic (TacCofix ido) (cofix ido)
-let h_mutual_cofix id l =
+let h_mutual_cofix b id l =
   abstract_tactic
-    (TacMutualCofix (id,List.map (fun (id,c) -> (id,inj_open c)) l)) 
+    (TacMutualCofix (b,id,List.map (fun (id,c) -> (id,inj_open c)) l)) 
     (mutual_cofix id l)
 
 let h_cut c          = abstract_tactic (TacCut (inj_open c)) (cut c)