diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-08 10:33:20 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-13 18:13:20 +0200 |
| commit | 9d0011125da2b24ccf006154ab205c6987fb03d2 (patch) | |
| tree | fb28bab986b15fb05e9d9ddbf0556f0a62f29b54 /library/global.ml | |
| parent | e62984e17cad223448feddeccac0d40e1f604c31 (diff) | |
library/opaqueTables: enable their use in interactive mode
Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).
With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
1) directly (before the constant is discharged)
2) indirectly, via an int, that is mapped by the opaque table to
the proof term.
This is now consistent in batch/interactive mode
This is step 0 to make an interactive coqtop able to dump a .vo/.vi
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/library/global.ml b/library/global.ml index 80238d8e2..49f78e495 100644 --- a/library/global.ml +++ b/library/global.ml @@ -113,6 +113,14 @@ let lookup_modtype kn = lookup_modtype kn (env()) let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ()) +let opaque_tables () = Environ.opaque_tables (env ()) +let body_of_constant_body cb = Declareops.body_of_constant (opaque_tables ()) cb +let body_of_constant cst = body_of_constant_body (lookup_constant cst) +let constraints_of_constant_body cb = + Declareops.constraints_of_constant (opaque_tables ()) cb +let universes_of_constant_body cb = + Declareops.universes_of_constant (opaque_tables ()) cb + (** Operations on kernel names *) let constant_of_delta_kn kn = @@ -153,7 +161,9 @@ let type_of_global_unsafe r = | VarRef id -> Environ.named_type id env | ConstRef c -> let cb = Environ.lookup_constant c env in - let univs = Declareops.universes_of_polymorphic_constant cb in + let univs = + Declareops.universes_of_polymorphic_constant + (Environ.opaque_tables env) cb in let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in Vars.subst_instance_constr (Univ.UContext.instance univs) ty | IndRef ind -> @@ -175,7 +185,9 @@ let type_of_global_in_context env r = | VarRef id -> Environ.named_type id env, Univ.UContext.empty | ConstRef c -> let cb = Environ.lookup_constant c env in - let univs = Declareops.universes_of_polymorphic_constant cb in + let univs = + Declareops.universes_of_polymorphic_constant + (Environ.opaque_tables env) cb in Typeops.type_of_constant_type env cb.Declarations.const_type, univs | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in @@ -198,7 +210,8 @@ let universes_of_global env r = | VarRef id -> Univ.UContext.empty | ConstRef c -> let cb = Environ.lookup_constant c env in - Declareops.universes_of_polymorphic_constant cb + Declareops.universes_of_polymorphic_constant + (Environ.opaque_tables env) cb | IndRef ind -> let (mib, oib) = Inductive.lookup_mind_specif env ind in Univ.instantiate_univ_context mib.mind_universes |