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 /kernel/declareops.mli | |
| 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 'kernel/declareops.mli')
| -rw-r--r-- | kernel/declareops.mli | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 04a067aff..497856676 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -28,15 +28,19 @@ val constant_has_body : constant_body -> bool (** Accessing const_body, forcing access to opaque proof term if needed. Only use this function if you know what you're doing. *) -val body_of_constant : constant_body -> Term.constr option +val body_of_constant : + Opaqueproof.opaquetab -> constant_body -> Term.constr option val type_of_constant : constant_body -> constant_type -val constraints_of_constant : constant_body -> Univ.constraints -val universes_of_constant : constant_body -> Univ.universe_context +val constraints_of_constant : + Opaqueproof.opaquetab -> constant_body -> Univ.constraints +val universes_of_constant : + Opaqueproof.opaquetab -> constant_body -> Univ.universe_context (** Return the universe context, in case the definition is polymorphic, otherwise the context is empty. *) -val universes_of_polymorphic_constant : constant_body -> Univ.universe_context +val universes_of_polymorphic_constant : + Opaqueproof.opaquetab -> constant_body -> Univ.universe_context val is_opaque : constant_body -> bool @@ -71,7 +75,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body -val join_constant_body : constant_body -> unit +val join_constant_body : Opaqueproof.opaquetab -> constant_body -> unit (** {6 Hash-consing} *) |