diff options
| author | Pierre-Marie Pédrot | 2020-09-22 14:19:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-21 12:20:10 +0200 |
| commit | 0590764209dcb8540b5292aca38fe2df38b90ab9 (patch) | |
| tree | cede5a6e0a7fabcfd55f7635604493876821afc6 /kernel/names.ml | |
| parent | 2b91a8989687e152f7120aa6c907ffeba8495bab (diff) | |
Same little game with Projection.
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index f987b1d92e..5f2ecea5f0 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -787,6 +787,8 @@ struct Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind) module SyntacticOrd = struct + type nonrec t = t + let compare a b = let c = ind_syntactic_ord a.proj_ind b.proj_ind in if c == 0 then Int.compare a.proj_arg b.proj_arg @@ -799,6 +801,8 @@ struct Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind) end module CanOrd = struct + type nonrec t = t + let compare a b = let c = ind_ord a.proj_ind b.proj_ind in if c == 0 then Int.compare a.proj_arg b.proj_arg @@ -811,6 +815,8 @@ struct Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind) end module UserOrd = struct + type nonrec t = t + let compare a b = let c = ind_user_ord a.proj_ind b.proj_ind in if c == 0 then Int.compare a.proj_arg b.proj_arg @@ -877,6 +883,7 @@ struct let hash (c, b) = (if b then 0 else 1) + Repr.hash c module SyntacticOrd = struct + type nonrec t = t let compare (c, b) (c', b') = if b = b' then Repr.SyntacticOrd.compare c c' else -1 let equal (c, b as x) (c', b' as x') = @@ -884,6 +891,7 @@ struct let hash (c, b) = (if b then 0 else 1) + Repr.SyntacticOrd.hash c end module CanOrd = struct + type nonrec t = t let compare (c, b) (c', b') = if b = b' then Repr.CanOrd.compare c c' else -1 let equal (c, b as x) (c', b' as x') = |