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.mli | |
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.mli')
-rw-r--r-- | kernel/vars.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/kernel/vars.mli b/kernel/vars.mli index b74d25260..3d3a26e90 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -137,6 +137,3 @@ val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Co (** Instance substitution for polymorphism. *) val subst_instance_constr : Instance.t -> constr -> constr val subst_instance_context : Instance.t -> Context.Rel.t -> Context.Rel.t - -type id_key = Constant.t tableKey -val eq_id_key : id_key -> id_key -> bool |