Anomaly "in Lemmas.save_lemma_admitted: more than one statement." with Derive

[SkySkimmer]

Require Import Derive.

Derive foo SuchThat True As bar.
Proof. Admitted.

Should be a regular error "Admitted does not support multiple statements" as is done in save_lemma_admitted_delayed
(in fact the delayed case should be the anomaly as multi statement proofs do not support delaying)

[herbelin]

coq/ceps#89 suggests that by postponing the computation of universes from before finish_admitted to within declare_possibly_mutual_parameter, we could compute the universes for each component of the block of theorems individually, relaxing the single-statement constraints. I'll have a look at it.

[SkySkimmer]

I don't think the error is about universes.

[herbelin]

Sorry, there was an implicit in my message namely that what apparently forced the restriction to one entry is that the current API expects only one universe entry, so if declare_possibly_mutual_parameter were computing itself the univs (one for each proof entry), we would not need the restriction to one entry.