diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 4 | ||||
| -rw-r--r-- | kernel/names.mli | 7 |
2 files changed, 11 insertions, 0 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index dfa73e95a1..463f47ca4c 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -416,3 +416,7 @@ let eq_id_key ik1 ik2 = ConstKey (_,kn1), ConstKey (_,kn2) -> kn1=kn2 | a,b -> a=b + +let eq_con_chk (kn1,_) (kn2,_) = kn1=kn2 +let eq_mind_chk (kn1,_) (kn2,_) = kn1=kn2 +let eq_ind_chk (kn1,i1) (kn2,i2) = i1=i2&&eq_mind_chk kn1 kn2 diff --git a/kernel/names.mli b/kernel/names.mli index 1c74fdee6d..74cebd22a8 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -229,3 +229,10 @@ type inv_rel_key = int (** index in the [rel_context] part of environment type id_key = inv_rel_key tableKey val eq_id_key : id_key -> id_key -> bool + +(*equalities on constant and inductive + names for the checker*) + +val eq_con_chk : constant -> constant -> bool +val eq_ind_chk : inductive -> inductive -> bool + |