diff options
Diffstat (limited to 'interp/constrextern.mli')
| -rw-r--r-- | interp/constrextern.mli | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli index d980b1995..51b06580e 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -60,6 +60,19 @@ val set_extern_reference : val get_extern_reference : unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) +(** WARNING: The following functions are evil due to + side-effects. Think of the following case as used in the printer: + + without_specific_symbols [SynDefRule kn] (pr_glob_constr_env env) c + + vs + + without_specific_symbols [SynDefRule kn] pr_glob_constr_env env c + + which one is wrong? We should turn this kind of state into an + explicit argument. +*) + (** This forces printing universe names of Type\{.\} *) val with_universes : ('a -> 'b) -> 'a -> 'b |