diff options
| author | Pierre-Marie Pédrot | 2016-09-07 18:51:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-08 16:55:46 +0200 |
| commit | ae9f6d13b63f30168d2eaa2289108a117ad840f7 (patch) | |
| tree | d937467dd5c1913960d58932df19853c93675acb /intf | |
| parent | dfac5aa2285de5b89f08ada3c30c0a1594737440 (diff) | |
Unplugging Tacexpr in several interface files.
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 = |