diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/misctypes.mli | 9 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 2 |
2 files changed, 10 insertions, 1 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 1452bbc347..c6c4b01e4e 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -108,3 +108,12 @@ type 'a or_by_notation = (** Kinds of modules *) type module_kind = Module | ModType | ModAny + +(** Various flags *) + +type direction_flag = bool (* true = Left-to-right false = right-to-right *) +type evars_flag = bool (* true = pose evars false = fail on evars *) +type rec_flag = bool (* true = recursive false = not recursive *) +type advanced_flag = bool (* true = advanced false = basic *) +type letin_flag = bool (* true = use local def false = use Leibniz *) +type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 946d124a45..cf33d79733 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -125,7 +125,7 @@ type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option type open_constr_expr = unit * constr_expr type open_glob_constr = unit * glob_constr_and_expr -type binding_bound_vars = Id.Set.t +type binding_bound_vars = Constr_matching.binding_bound_vars type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern type 'a delayed_open = 'a Pretyping.delayed_open = |