Avoid retypechecking repeated subterms in typeops

kernel/constr.ml

@@ -1147,8 +1147,8 @@ let invert_eqeq iv1 iv2 =
 let hasheq_ctx (nas1, c1) (nas2, c2) =
   array_eqeq nas1 nas2 && c1 == c2
 
-let hasheq t1 t2 =
-  match kind t1, kind t2 with
+let hasheq_kind t1 t2 =
+  match t1, t2 with
     | Rel n1, Rel n2 -> n1 == n2
     | Meta m1, Meta m2 -> m1 == m2
     | Var id1, Var id2 -> id1 == id2
@@ -1189,6 +1189,8 @@ let hasheq t1 t2 =
       | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _
       | Fix _ | CoFix _ | Int _ | Float _ | String _ | Array _), _ -> false
 
+let hasheq t1 t2 = hasheq_kind (kind t1) (kind t2)
+
 (** Note that the following Make has the side effect of creating
     once and for all the table we'll use for hash-consing all constr *)
 

kernel/constr.mli

@@ -630,6 +630,9 @@ val case_info_hash : case_info -> int
 
 val hcons : constr -> constr
 
+val hasheq_kind : (_ kind_of_term as 'k) -> 'k -> bool
+(** Checks physical equality of every immediate element (goes inside tuples and arrays) *)
+
 val debug_print : constr -> Pp.t
 val debug_print_fix : ('a -> Pp.t) -> ('a, 'a, 'r) pfixpoint -> Pp.t
 
@@ -641,3 +644,9 @@ val mkInd : inductive -> constr
 
 val mkConstruct : constructor -> constr
 [@@deprecated "Use [mkConstructU] or if truly needed [UnsafeMonomorphic.mkConstruct]"]
+
+val hcons_annot : Name.t binder_annot -> Name.t binder_annot
+
+val hcons_caseinfo : case_info -> case_info
+
+val hash_cast_kind : cast_kind -> int