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/subtyping.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'kernel/subtyping.ml') diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 4f54220e7..857f577a8 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -352,7 +352,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let u1 = inductive_instance mind1 in let arity1,cst1 = constrained_type_of_inductive env ((mind1,mind1.mind_packets.(i)),u1) in - let cst2 = Declareops.constraints_of_constant cb2 in + let cst2 = + Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in let typ2 = Typeops.type_of_constant_type env cb2.const_type in let cst = Constraint.union cst (Constraint.union cst1 cst2) in let error = NotConvertibleTypeField (env, arity1, typ2) in @@ -367,7 +368,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; let u1 = inductive_instance mind1 in let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in - let cst2 = Declareops.constraints_of_constant cb2 in + let cst2 = + Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in let ty2 = Typeops.type_of_constant_type env cb2.const_type in let cst = Constraint.union cst (Constraint.union cst1 cst2) in let error = NotConvertibleTypeField (env, ty1, ty2) in -- cgit v1.2.3