Jason Gross (Oct 18 2022 at 15:43): Jason Gross (Oct 18 2022 at 15:43):What's up with https://github.com/coq/coq/blob/d9d51353214eb04dea89285b1a8713a92b9d82b2/kernel/constr.ml#L902 (" (* Why do we suddenly make a special case for Cast here? *)") in
| LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq 0 b1 b2 && eq 0 t1 t2 && leq nargs c1 c2
(* Why do we suddenly make a special case for Cast here? *)
| App (c1, l1), App (c2, l2) ->
let len = Array.length l1 in
Int.equal len (Array.length l2) &&
leq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2
forgot to remove it in bc26ad1cbbeb0a8aa2ac36916db3c09330bacfd0
Jason Gross (Oct 18 2022 at 16:34):Fixed in https://github.com/coq/coq/pull/16694
Last updated: Oct 13 2024 at 01:02 UTC