Same little game with Projection.

6 files changed, 22 insertions, 9 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') =
diff --git a/kernel/names.mli b/kernel/names.mli
index 9a01ea2b43..a0320fda43 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -565,16 +565,19 @@ module Projection : sig
     val make : inductive -> proj_npars:int -> proj_arg:int -> Label.t -> t
 
     module SyntacticOrd : sig
+      type nonrec t = t
       val compare : t -> t -> int
       val equal : t -> t -> bool
       val hash : t -> int
     end
     module CanOrd : sig
+      type nonrec t = t
       val compare : t -> t -> int
       val equal : t -> t -> bool
       val hash : t -> int
     end
     module UserOrd : sig
+      type nonrec t = t
       val compare : t -> t -> int
       val equal : t -> t -> bool
       val hash : t -> int
@@ -589,9 +592,9 @@ module Projection : sig
     val arg : t -> int
     val label : t -> Label.t
 
-    val equal : t -> t -> bool
-    val hash : t -> int
-    val compare : t -> t -> int
+    val equal : t -> t -> bool [@@ocaml.deprecated "Use QProjection.equal"]
+    val hash : t -> int [@@ocaml.deprecated "Use QProjection.hash"]
+    val compare : t -> t -> int [@@ocaml.deprecated "Use QProjection.compare"]
 
     val map : (MutInd.t -> MutInd.t) -> t -> t
     val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t
@@ -609,11 +612,13 @@ module Projection : sig
   val repr : t -> Repr.t
 
   module SyntacticOrd : sig
+    type nonrec t = t
     val compare : t -> t -> int
     val equal : t -> t -> bool
     val hash : t -> int
   end
   module CanOrd : sig
+    type nonrec t = t
     val compare : t -> t -> int
     val equal : t -> t -> bool
     val hash : t -> int
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index f295b36b60..8eb1c10f70 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -441,7 +441,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         | Some s2 ->
           eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
         | None ->
-          if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2)
+          if Projection.Repr.CanOrd.equal (Projection.repr p1) (Projection.repr p2)
              && compare_stack_shape v1 v2 then
             let el1 = el_stack lft1 v1 in
             let el2 = el_stack lft2 v2 in
@@ -704,7 +704,7 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
             | (Zlapp a1,Zlapp a2) ->
                Array.fold_right2 f a1 a2 cu1
             | (Zlproj (c1,_l1),Zlproj (c2,_l2)) ->
-              if not (Projection.Repr.equal c1 c2) then
+              if not (Projection.Repr.CanOrd.equal c1 c2) then
                 raise NotConvertible
               else cu1
             | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 948195797e..2de902c827 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -141,7 +141,7 @@ and conv_stack env k stk1 stk2 cu =
         conv_stack env k stk1 stk2 !rcu
       else raise NotConvertible
   | Zproj p1 :: stk1, Zproj p2 :: stk2 ->
-    if Projection.Repr.equal p1 p2 then conv_stack env k stk1 stk2 cu
+    if Projection.Repr.CanOrd.equal p1 p2 then conv_stack env k stk1 stk2 cu
     else raise NotConvertible
   | [], _ | Zapp _ :: _, _ | Zfix _ :: _, _ | Zswitch _ :: _, _
   | Zproj _ :: _, _ -> raise NotConvertible
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index 42908a7363..babc57794b 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -38,7 +38,7 @@ let eq_reloc_info r1 r2 = match r1, r2 with
 | Reloc_const _, _ -> false
 | Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.CanOrd.equal c1 c2
 | Reloc_getglobal _, _ -> false
-| Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.equal p1 p2
+| Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.CanOrd.equal p1 p2
 | Reloc_proj_name _, _ -> false
 | Reloc_caml_prim p1, Reloc_caml_prim p2 -> CPrimitives.equal p1 p2
 | Reloc_caml_prim _, _ -> false
@@ -49,7 +49,7 @@ let hash_reloc_info r =
   | Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw)
   | Reloc_const c -> combinesmall 2 (hash_structured_constant c)
   | Reloc_getglobal c -> combinesmall 3 (Constant.CanOrd.hash c)
-  | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.hash p)
+  | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.CanOrd.hash p)
   | Reloc_caml_prim p -> combinesmall 5 (CPrimitives.hash p)
 
 module RelocTable = Hashtbl.Make(struct
diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml
index 9d80dc578b..ae0fa38571 100644
--- a/kernel/vmsymtable.ml
+++ b/kernel/vmsymtable.ml
@@ -85,7 +85,7 @@ module AnnotTable = Hashtbl.Make (struct
   let hash = hash_annot_switch
 end)
 
-module ProjNameTable = Hashtbl.Make (Projection.Repr)
+module ProjNameTable = Hashtbl.Make (Projection.Repr.CanOrd)
 
 let str_cst_tbl : int SConstTable.t = SConstTable.create 31