Stream: Coq devs & plugin devs

Topic: Confusing comment in the kernel


view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Oct 18 2022 at 15:48):

forgot to remove it in bc26ad1cbbeb0a8aa2ac36916db3c09330bacfd0

view this post on Zulip 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