aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/wcclausenv.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/wcclausenv.mli')
-rw-r--r--tactics/wcclausenv.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index 26c46e89a..45b955326 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -45,6 +45,6 @@ val add_prods_sign :
**i*)
val elim_res_pf_THEN_i :
- (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> tactic
+ (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic array) -> tactic
val applyUsing : constr -> tactic