search

LPCIC / coq-elpi

Coq plugin embedding elpi
GNU Lesser General Public License v2.1
134 stars 50 forks source link

coq.env.add-indt fails to add universe polymorphic inductives when not in a section #387

Open ecranceMERCE opened 2 years ago

ecranceMERCE commented 2 years ago

Declaring a new universe polymorphic inductive type with coq.env.add-indt fails when not in a section.

From elpi Require Import elpi.
Set Universe Polymorphism.

Elpi Tactic test.

(* Section Test. *)

Elpi Query lp:{{
  coq.univ.new U,
  coq.univ.variable U L,
  @udecl! [L] tt [] tt =>
    coq.env.add-indt (inductive "MyFalse" tt (arity (sort (typ U))) (i\ [])) I.
}}.
No open section.

Uncommenting the line before the Elpi query makes the error vanish.

ecranceMERCE commented 2 years ago

Issue https://github.com/LPCIC/coq-elpi/issues/374 might be related as the error message is the same.

ecranceMERCE commented 1 year ago

I think this bug came from the fact I tried to edit poly in this line, so maybe I opened an issue that does not concern master, and if that's the case I am sorry.

Nevertheless, I still do not understand why everything works even when leaving this boolean to false. It's counter-intuitive to declare polymorphic inductives by saying the universe context is not polymorphic...

But in the Coq API, it calls some section function in the poly case, which causes the bug if the boolean is true.