Stream: Coq users

Topic: ✔ Context match bug

Paolo Giarrusso (Oct 07 2022 at 19:12):

printing universes reveals the two arguments have different universes, while with the stdlib no universes appear. I don't know if that's supposed to count as "syntactically different", but that would be reasonable

t@{hott.67}
           (underlying_natural@{hott.74 hott.75} (S n)
              (s@{hott.76 hott.77 hott.78 hott.79 hott.74 hott.75} n i y1))
           (underlying_natural@{hott.82 hott.83} (S n)
              (s@{hott.76 hott.77 hott.78 hott.79 hott.82 hott.83} n i y1))

Paolo Giarrusso (Oct 07 2022 at 19:14):

Meanwhile, this works, but has a very different meaning. unify can perform lots of computation in general

  match goal with
  | [ H : lt ?n1 ?n2 |- _ ] => unify n1 n2; idtac n1 n2
  end.

Gaëtan Gilbert (Oct 07 2022 at 19:14):

constr_eq should be enough

Paolo Giarrusso (Oct 07 2022 at 19:18):

yep

Patrick Nicodemus (Oct 07 2022 at 19:24):

nice thanks!

Notification Bot (Oct 07 2022 at 19:24):

Patrick Nicodemus has marked this topic as resolved.

Last updated: Feb 06 2023 at 12:04 UTC