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 8aee8dcb7..b1bf17e01 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -46,7 +46,7 @@ val res_pf_THEN_i :
(wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) ->
int -> tactic
-val elim_res_pf_THEN_id :
+val elim_res_pf_THEN_i :
(wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) ->
int -> tactic