aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacticals.mli')
-rw-r--r--tactics/tacticals.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index e7d8cff25..f863bad68 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -53,7 +53,7 @@ val matches : goal sigma -> constr -> marked_term -> bool
val dest_match : goal sigma -> constr -> marked_term -> constr list
*)
(* The second argument is the pattern *)
-val matches : goal sigma -> constr -> constr -> bool
+val matches : goal sigma -> constr -> marked_pattern -> bool
val dest_match : goal sigma -> constr -> constr -> constr list
val allHyps : goal sigma -> clause list