From 2cb554aa772c5c6d179c6a4611b70d459073a316 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 20 Dec 2015 01:04:15 +0100 Subject: Exporting a generic argument induction_arg. As a consequence, simplifying and generalizing the grammar entries for injection, discriminate and simplify_eq. --- intf/tacexpr.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 35e6a2e31..5b5957bef 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -40,13 +40,13 @@ type goal_selector = | SelectId of Id.t | SelectAll -type 'a core_induction_arg = +type 'a core_destruction_arg = | ElimOnConstr of 'a | ElimOnIdent of Id.t located | ElimOnAnonHyp of int -type 'a induction_arg = - clear_flag * 'a core_induction_arg +type 'a destruction_arg = + clear_flag * 'a core_destruction_arg type inversion_kind = | SimpleInversion @@ -68,7 +68,7 @@ type 'id message_token = | MsgIdent of 'id type ('dconstr,'id) induction_clause = - 'dconstr with_bindings induction_arg * + 'dconstr with_bindings destruction_arg * (intro_pattern_naming_expr located option (* eqn:... *) * 'dconstr or_and_intro_pattern_expr located or_var option) (* as ... *) * 'id clause_expr option (* in ... *) -- cgit v1.2.3