From e82856f3108a25f7b0cabff4190bc56d3a0cafa1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 30 Jul 2017 16:10:14 +0200 Subject: Handling evars in the VM. We simply treat them as as an application of an atom to its instance, and in the decompilation phase we reconstruct the instance from the stack. This grants wish BZ#5659. --- kernel/vars.ml | 3 --- 1 file changed, 3 deletions(-) (limited to 'kernel/vars.ml') diff --git a/kernel/vars.ml b/kernel/vars.ml index b3b3eff62..56d3f11b9 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -310,6 +310,3 @@ let subst_instance_constr subst c = let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx else Context.Rel.map (fun x -> subst_instance_constr s x) ctx - -type id_key = Constant.t tableKey -let eq_id_key x y = Names.eq_table_key Constant.equal x y -- cgit v1.2.3