diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-20 01:04:15 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-18 13:07:22 +0200 |
| commit | 2cb554aa772c5c6d179c6a4611b70d459073a316 (patch) | |
| tree | 4493ad52bb7adf03128de2bba63d46f26a893a77 /intf | |
| parent | 403af31e3d0bc571acf0a66907277ad839c94df4 (diff) | |
Exporting a generic argument induction_arg. As a consequence,
simplifying and generalizing the grammar entries for injection,
discriminate and simplify_eq.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 8 |
1 files changed, 4 insertions, 4 deletions
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 ... *) |