From 9d0011125da2b24ccf006154ab205c6987fb03d2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 8 Oct 2014 10:33:20 +0200 Subject: 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 --- kernel/mod_typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index cab3276c3..7a9b12c43 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -72,7 +72,7 @@ let rec check_with_def env struc (idl,c) mp equiv = (* In the spirit of subtyping.check_constant, we accept any implementations of parameters and opaques terms, as long as they have the right type *) - let ccst = Declareops.constraints_of_constant cb in + let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in let env' = Environ.add_constraints ccst env' in let c',cst = match cb.const_body with | Undef _ | OpaqueDef _ -> -- cgit v1.2.3