diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:34:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:52:43 +0200 |
| commit | cd139311ecd872301077b9db2df812a828ce2e77 (patch) | |
| tree | ed253a65a1a47df06d2bb1784bb62207782b83cc /kernel/reduction.ml | |
| parent | 3e57bde4e0ff1b9f65976f2de4d48a78131d4db3 (diff) | |
Fixing an incompatility introduced in a404360: kernel conversion was
not considering conversion of constants over their canonical name but
on their user name. This is observable when delta is off.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 97c3e1b34..2f1df396b 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -193,7 +193,7 @@ let convert_instances ~flex u u' (s, check) = let conv_table_key infos k1 k2 cuniv = if k1 == k2 then cuniv else match k1, k2 with - | ConstKey (cst, u), ConstKey (cst', u') when eq_constant_key cst cst' -> + | ConstKey (cst, u), ConstKey (cst', u') when Constant.equal cst cst' -> if Univ.Instance.equal u u' then cuniv else let flex = evaluable_constant cst (info_env infos) |