aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/nativecode.ml6
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