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/declare.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/declare.ml')
| -rw-r--r-- | library/declare.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/library/declare.ml b/library/declare.ml index 1c9e10a19..4ec81c49f 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -116,7 +116,7 @@ let open_constant i ((sp,kn), obj) = match (Global.lookup_constant con).const_body with | (Def _ | Undef _) -> () | OpaqueDef lc -> - match Opaqueproof.get_constraints lc with + match Opaqueproof.get_constraints (Global.opaque_tables ())lc with | Some f when Future.is_val f -> Global.push_context_set (Future.force f) | _ -> () @@ -208,7 +208,8 @@ let declare_sideff env fix_exn se = match cb with | { const_body = Def sc } -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false | { const_body = OpaqueDef fc } -> - (Opaqueproof.force_proof fc, Opaqueproof.force_constraints fc), true + (Opaqueproof.force_proof (Environ.opaque_tables env) fc, + Opaqueproof.force_constraints (Environ.opaque_tables env) fc), true | { const_body = Undef _ } -> anomaly(str"Undefined side effect") in let ty_of cb = |