diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/locus.mli | 6 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 6 |
2 files changed, 9 insertions, 3 deletions
diff --git a/intf/locus.mli b/intf/locus.mli index e0ce43331e..35b7380645 100644 --- a/intf/locus.mli +++ b/intf/locus.mli @@ -86,3 +86,9 @@ type goal_location = hyp_location option the conclusion (conclusion is represented by None) *) type simple_clause = Id.t option list + +(** {6 A notion of occurrences allowing to express "all occurrences + convertible to the first which matches"} *) + +type 'a or_like_first = AtOccs of 'a | LikeFirst + diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 2967c10dd7..c8c7e28e9f 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -56,15 +56,15 @@ type 'id message_token = | MsgInt of int | MsgIdent of 'id -type 'constr induction_clause = +type ('constr,'id) induction_clause = 'constr with_bindings induction_arg * (intro_pattern_naming_expr located option (* eqn:... *) * 'constr or_and_intro_pattern_expr located or_var option) (* as ... *) + * 'id clause_expr option (* in ... *) type ('constr,'id) induction_clause_list = - 'constr induction_clause list + ('constr,'id) induction_clause list * 'constr with_bindings option (* using ... *) - * 'id clause_expr option (* in ... *) type 'a with_bindings_arg = clear_flag * 'a with_bindings |