diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-30 16:10:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-03 18:05:56 +0100 |
| commit | e82856f3108a25f7b0cabff4190bc56d3a0cafa1 (patch) | |
| tree | 712336a242276c7ceb9dcde72999ad0769faa669 /kernel/vars.ml | |
| parent | df9d3a36e71d6d224286811fdc529ad5a955deb7 (diff) | |
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.
Diffstat (limited to 'kernel/vars.ml')
| -rw-r--r-- | kernel/vars.ml | 3 |
1 files changed, 0 insertions, 3 deletions
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 |