diff options
| author | coqbot-app[bot] | 2020-11-26 11:06:00 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-26 11:06:00 +0000 |
| commit | 0fc82e9651ee1dbc429c9b328b90ad8ad1a3cb14 (patch) | |
| tree | c99091031ad585bf3249ae089e12f44d4e5d83ce /kernel | |
| parent | 5c7f71a270b265d1ae3f86cb2a29d28f2310edc5 (diff) | |
| parent | 4011a9137fdebe16aa40cb03ba5ce32c09687c69 (diff) | |
Merge PR #13415: Separate interning and pretyping of universes
Reviewed-by: mattam82
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 2 | ||||
| -rw-r--r-- | kernel/names.mli | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 13761ca245..be65faf234 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1115,3 +1115,5 @@ let eq_egr e1 e2 = match e1, e2 with type lident = Id.t CAst.t type lname = Name.t CAst.t type lstring = string CAst.t + +let lident_eq = CAst.eq Id.equal diff --git a/kernel/names.mli b/kernel/names.mli index 74a4e6f7d0..747299bb12 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -727,3 +727,5 @@ val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool type lident = Id.t CAst.t type lname = Name.t CAst.t type lstring = string CAst.t + +val lident_eq : lident -> lident -> bool |