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 01b9e5e93..5a4ecbac7 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -263,5 +263,5 @@ module New : sig
val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
- val pf_constr_of_global : Globnames.global_reference -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic
+ val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic
end