diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-24 15:03:34 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-24 15:04:30 +0200 |
| commit | 9ec08ac299faf6acdfd6061fd21a00e3446aec79 (patch) | |
| tree | 2eed6d251673b4707696632380cd76d724136fff /intf | |
| parent | e24a118644d77e86ace11a34230711b204025c3b (diff) | |
Using an or_var rather than the hack with loc for coding a pure ident
as a disjunctive intropattern.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 3501917f2..2967c10dd 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -44,9 +44,9 @@ type inversion_kind = type ('c,'id) inversion_strength = | NonDepInversion of - inversion_kind * 'id list * 'c or_and_intro_pattern_expr located option + inversion_kind * 'id list * 'c or_and_intro_pattern_expr located or_var option | DepInversion of - inversion_kind * 'c option * 'c or_and_intro_pattern_expr located option + inversion_kind * 'c option * 'c or_and_intro_pattern_expr located or_var option | InversionUsing of 'c * 'id list type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b @@ -59,7 +59,7 @@ type 'id message_token = type 'constr induction_clause = 'constr with_bindings induction_arg * (intro_pattern_naming_expr located option (* eqn:... *) - * 'constr or_and_intro_pattern_expr located option) (* as ... *) + * 'constr or_and_intro_pattern_expr located or_var option) (* as ... *) type ('constr,'id) induction_clause_list = 'constr induction_clause list |