aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/elim.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/elim.mli')
-rw-r--r--tactics/elim.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/elim.mli b/tactics/elim.mli
index a1af31c6b..d135997cd 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -23,7 +23,7 @@ val introCaseAssumsThen :
(intro_pattern_expr Loc.located list -> branch_assumptions -> tactic) ->
branch_args -> tactic
-val general_decompose : (identifier * constr -> bool) -> constr -> tactic
+val general_decompose : (Id.t * constr -> bool) -> constr -> tactic
val decompose_nonrec : constr -> tactic
val decompose_and : constr -> tactic
val decompose_or : constr -> tactic