Cleaning/uniformizing the interface of tacticals.mli

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

4 files changed, 15 insertions, 4 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 7a66067cd7..9dd35a8c23 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -448,8 +448,9 @@ let rec tclTHENLIST = function
     [] -> tclIDTAC
   | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl)
 
-
-
+(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
+let tclMAP tacfun l = 
+  List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
 
 (* various progress criterions *)
 let same_goal gl subgoal = 
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 1823514270..5cbc2bde8f 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -80,6 +80,9 @@ val tclTHEN          : tactic -> tactic -> tactic
    convenient than [tclTHEN] when [n] is large *)
 val tclTHENLIST      : tactic list -> tactic
 
+(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
+val tclMAP           : ('a -> tactic) -> 'a list -> tactic
+
 (* [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
    [(tac2 i)] to the [i]$^{th}$ resulting subgoal (starting from 1) *)
 val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index f9b7b8677d..fa22de7bb2 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -111,11 +111,14 @@ let pf_const_value              = pf_reduce (fun env _ -> constant_value env)
 let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
 let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
-let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls)
+let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls)
 
 let pf_check_type gls c1 c2 = 
   ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2)))
 
+let pf_is_matching              = pf_apply Matching.is_matching_conv
+let pf_matches                  = pf_apply Matching.matches_conv
+
 (************************************)
 (* Tactics handling a list of goals *)
 (************************************)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index f57b121dba..826337cc8d 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -21,6 +21,7 @@ open Refiner
 open Redexpr
 open Tacexpr
 open Rawterm
+open Pattern
 (*i*)
 
 (* Operations for handling terms under a local typing context. *)
@@ -51,7 +52,7 @@ val pf_global             : goal sigma -> identifier -> constr
 val pf_parse_const        : goal sigma -> string -> constr
 val pf_type_of            : goal sigma -> constr -> types
 val pf_check_type         : goal sigma -> constr -> types -> unit
-val hnf_type_of           : goal sigma -> constr -> types
+val pf_hnf_type_of        : goal sigma -> constr -> types
 
 val pf_interp_constr      : goal sigma -> Topconstr.constr_expr -> constr
 val pf_interp_type        : goal sigma -> Topconstr.constr_expr -> types
@@ -86,6 +87,9 @@ val pf_const_value : goal sigma -> constant -> constr
 val pf_conv_x      : goal sigma -> constr -> constr -> bool
 val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
 
+val pf_matches     : goal sigma -> constr_pattern -> constr -> patvar_map
+val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
+
 type transformation_tactic = proof_tree -> (goal list * validation)
 
 val frontier : transformation_tactic