diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 19:08:35 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-21 18:04:32 +0100 |
| commit | 0ddf7d9c35eb2dd5f368e7a5735970ef1fd41fc6 (patch) | |
| tree | 0bc32293ac19ddd63cf764ccbd224b086c7836bc /interp/constrextern.mli | |
| parent | b75beb248873db7d9ab8e4a078022b2ed0edcd36 (diff) | |
[printing] Deprecate all printing functions accessing the global proof.
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
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 |