diff options
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index 9fbe7d5e5..d82043da1 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -458,11 +458,8 @@ type inv_rel_key = int (** index in the [rel_context] part of environment starting by the end, {e inverse} of de Bruijn indice *) -type id_key = Constant.t tableKey - val eq_table_key : ('a -> 'a -> bool) -> 'a tableKey -> 'a tableKey -> bool val eq_constant_key : Constant.t -> Constant.t -> bool -val eq_id_key : id_key -> id_key -> bool (** equalities on constant and inductive names (for the checker) *) |