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, 20 insertions, 18 deletions

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 0cb3142013..c3b7e0a8ba 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)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 8cbc28d1ec..49415649bd 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -43,10 +43,11 @@ val h_elim_type       : constr -> tactic
 val h_case            : evars_flag -> constr with_ebindings -> tactic
 val h_case_type       : constr -> tactic
 
-val h_mutual_fix      : identifier -> int ->
+val h_mutual_fix      : hidden_flag -> identifier -> int ->
                         (identifier * int * constr) list -> tactic
 val h_fix             : identifier option -> int -> tactic
-val h_mutual_cofix    : identifier -> (identifier * constr) list -> tactic
+val h_mutual_cofix    : hidden_flag -> identifier -> 
+                        (identifier * constr) list -> tactic
 val h_cofix           : identifier option -> tactic
 
 val h_cut             : constr -> tactic 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3367f89f18..068ae8e963 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -657,13 +657,13 @@ let rec intern_atomic lf ist x =
   | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb)
   | TacCaseType c -> TacCaseType (intern_type ist c)
   | TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n)
-  | TacMutualFix (id,n,l) ->
+  | TacMutualFix (b,id,n,l) ->
       let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
-      TacMutualFix (intern_ident lf ist id, n, List.map f l)
+      TacMutualFix (b,intern_ident lf ist id, n, List.map f l)
   | TacCofix idopt -> TacCofix (Option.map (intern_ident lf ist) idopt)
-  | TacMutualCofix (id,l) ->
+  | TacMutualCofix (b,id,l) ->
       let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
-      TacMutualCofix (intern_ident lf ist id, List.map f l)
+      TacMutualCofix (b,intern_ident lf ist id, List.map f l)
   | TacCut c -> TacCut (intern_type ist c)
   | TacAssert (otac,ipat,c) ->
       TacAssert (Option.map (intern_tactic ist) otac,
@@ -2016,13 +2016,13 @@ and interp_atomic ist gl = function
   | TacCase (ev,cb) -> h_case ev (interp_constr_with_bindings ist gl cb)
   | TacCaseType c -> h_case_type (pf_interp_type ist gl c)
   | TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist gl) idopt) n
-  | TacMutualFix (id,n,l) ->
+  | TacMutualFix (b,id,n,l) ->
       let f (id,n,c) = (interp_fresh_ident ist gl id,n,pf_interp_type ist gl c)
-      in h_mutual_fix (interp_fresh_ident ist gl id) n (List.map f l)
+      in h_mutual_fix b (interp_fresh_ident ist gl id) n (List.map f l)
   | TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist gl) idopt)
-  | TacMutualCofix (id,l) ->
+  | TacMutualCofix (b,id,l) ->
       let f (id,c) = (interp_fresh_ident ist gl id,pf_interp_type ist gl c) in
-      h_mutual_cofix (interp_fresh_ident ist gl id) (List.map f l)
+      h_mutual_cofix b (interp_fresh_ident ist gl id) (List.map f l)
   | TacCut c -> h_cut (pf_interp_type ist gl c)
   | TacAssert (t,ipat,c) ->
       let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in
@@ -2350,11 +2350,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacCase (ev,cb) -> TacCase (ev,subst_raw_with_bindings subst cb)
   | TacCaseType c -> TacCaseType (subst_rawconstr subst c)
   | TacFix (idopt,n) as x -> x
-  | TacMutualFix (id,n,l) ->
-      TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_rawconstr subst c)) l)
+  | TacMutualFix (b,id,n,l) ->
+      TacMutualFix(b,id,n,List.map (fun (id,n,c) -> (id,n,subst_rawconstr subst c)) l)
   | TacCofix idopt as x -> x
-  | TacMutualCofix (id,l) ->
-      TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
+  | TacMutualCofix (b,id,l) ->
+      TacMutualCofix (b,id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
   | TacCut c -> TacCut (subst_rawconstr subst c)
   | TacAssert (b,na,c) ->
       TacAssert (Option.map (subst_tactic subst) b,na,subst_rawconstr subst c)