diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-26 14:51:32 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-26 14:51:32 +0200 |
| commit | fb9c581491715c4c34054a744426318a6991c9ed (patch) | |
| tree | 1a135ed44356123077dc1d3eff7cb3d67ef23add /kernel | |
| parent | 7cc9bbd2c3f9faf4bbf66cae1bbd07289819161a (diff) | |
| parent | 13bde6f161f2ebe5108023a7e0d3696f2a305719 (diff) | |
Merge PR #7919: Fix equality check on global names from native compute.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/nativecode.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 6821fc980..74d12f3cd 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -71,6 +71,8 @@ let eq_gname gn1 gn2 = String.equal s1 s2 && eq_constructor c1 c2 | Gconstant (s1, c1), Gconstant (s2, c2) -> String.equal s1 s2 && Constant.equal c1 c2 + | Gproj (s1, ind1, i1), Gproj (s2, ind2, i2) -> + String.equal s1 s2 && eq_ind ind1 ind2 && Int.equal i1 i2 | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2 | Gcase (Some l1, i1), Gcase (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2 | Gpred (None, i1), Gpred (None, i2) -> Int.equal i1 i2 @@ -86,7 +88,9 @@ let eq_gname gn1 gn2 = | Ginternal s1, Ginternal s2 -> String.equal s1 s2 | Grel i1, Grel i2 -> Int.equal i1 i2 | Gnamed id1, Gnamed id2 -> Id.equal id1 id2 - | _ -> false + | (Gind _| Gconstruct _ | Gconstant _ | Gproj _ | Gcase _ | Gpred _ + | Gfixtype _ | Gnorm _ | Gnormtbl _ | Ginternal _ | Grel _ | Gnamed _), _ -> + false let dummy_gname = Grel 0 |