Karl Palmskog (Jan 08 2023 at 15:50): Karl Palmskog (Jan 08 2023 at 15:50):coq-elpi.dev is seemingly broken with some versions of OCaml/packages:
# CAMLC -c src/coq_elpi_builtins.mli
# CAMLC -c src/coq_elpi_vernacular.ml
# CAMLC -c src/coq_elpi_utils.ml
# CAMLC -c src/coq_elpi_HOAS.ml
# File "src/coq_elpi_HOAS.ml", line 176, characters 6-17:
# 176 | | Sorts.QSort _ -> Format.fprintf fmt "Type");
# ^^^^^^^^^^^
# Error: Unbound constructor Sorts.QSort
Some dependency issue?
Karl Palmskog (Jan 08 2023 at 16:24):happens on OCaml 4.14.0 and 5.0.0, but not 4.11.1.
Enrico Tassi (Jan 09 2023 at 20:22):I was late merging an overlay PR, it should be fine now
Karl Palmskog (Jan 18 2023 at 09:00):I'm guessing this is also due to pending overlay:
# CAMLC -c src/coq_elpi_utils.ml
# File "src/coq_elpi_utils.ml", line 226, characters 42-60:
# 226 | options (Detyping.detype Detyping.Now Names.Id.Set.empty env sigma) t in
# ^^^^^^^^^^^^^^^^^^
# Error: This expression has type Names.Id.Set.t
# but an expression was expected of type bool
I think I've merged the overlay for that one already: https://github.com/LPCIC/coq-elpi/pull/425#event-8240961694
Can you please retry?
Karl Palmskog (Jan 18 2023 at 19:35):works now, thanks
Last updated: Jun 06 2023 at 22:01 UTC