diff options
| author | Maxime Dénès | 2017-06-14 15:08:08 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-14 15:08:08 +0200 |
| commit | aed7a86b2147e70bebd50a4d19bac33908da334b (patch) | |
| tree | 8eb38b87a2492692244130c10e3e17fccaf242e8 /interp/constrextern.mli | |
| parent | 9a3aba3677686c1e93a04e27f94414c0d6643c42 (diff) | |
| parent | d50923b778684a2ffcc211beb5341a54304c97a4 (diff) | |
Merge PR#703: New version of the selective-unfolding PR
Diffstat (limited to 'interp/constrextern.mli')
| -rw-r--r-- | interp/constrextern.mli | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli index ea627cff11..d771ee86fb 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -80,3 +80,13 @@ val without_specific_symbols : interp_rule list -> ('a -> 'b) -> 'a -> 'b (** This prints metas as anonymous holes *) val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b + +(** Fine-grained activation and deactivation of notation printing. + *) +val toggle_scope_printing : + scope:Notation_term.scope_name -> activate:bool -> unit + +val toggle_notation_printing : + ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit + + |