Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 10 insertions, 10 deletions

diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 37acf850..a808ca41 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacmach.mli 12168 2009-06-06 21:34:37Z herbelin $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -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
@@ -66,12 +67,12 @@ val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> constr
 
 
 val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
-val pf_reduce : 
+val pf_reduce :
   (env -> evar_map -> constr -> constr) ->
     goal sigma -> constr -> constr
 
 val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
-val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list 
+val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list
 val pf_hnf_constr              : goal sigma -> constr -> constr
 val pf_red_product             : goal sigma -> constr -> constr
 val pf_nf                      : goal sigma -> constr -> constr
@@ -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
@@ -106,7 +110,7 @@ val weak_undo_pftreestate   : pftreestate -> pftreestate
 val solve_nth_pftreestate   : int -> tactic -> pftreestate -> pftreestate
 val solve_pftreestate       : tactic -> pftreestate -> pftreestate
 val mk_pftreestate          : goal -> pftreestate
-val extract_open_pftreestate : pftreestate -> constr * Termops.metamap
+val extract_open_pftreestate : pftreestate -> constr * Termops.meta_type_map
 val extract_pftreestate     : pftreestate -> constr
 val first_unproven          : pftreestate -> pftreestate
 val last_unproven           : pftreestate -> pftreestate
@@ -135,12 +139,8 @@ val move_hyp_no_check         :
 val rename_hyp_no_check       : (identifier*identifier) list -> tactic
 val order_hyps : identifier list -> tactic
 val mutual_fix      :
-  identifier -> int -> (identifier * int * constr) list -> tactic
-val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
-val mutual_fix_with_index :
   identifier -> int -> (identifier * int * constr) list -> int -> tactic
-val mutual_cofix_with_index : 
-  identifier -> (identifier * constr) list -> int -> tactic
+val mutual_cofix    : identifier -> (identifier * constr) list -> int -> tactic
 
 (*s The most primitive tactics with consistency and type checking *)