diff options
| -rw-r--r-- | interp/constrextern.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli index d49b2b9a73..2aa16c8c33 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -58,3 +58,6 @@ val with_universes : ('a -> 'b) -> 'a -> 'b (* This suppresses printing of numeral and symbols *) val without_symbols : ('a -> 'b) -> 'a -> 'b + +(* This prints metas as anonymous holes *) +val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b |