The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

This is an error from calling constr_of_global (from module Universes, 
in Coq master from module UnivGen) on some universe polymorphic global.

Tacmach.pf_global is a wrapper of it. You're unlikely to be using any 
other caller in an ocaml tactic.

This is a function to turn a constant or inductive into a term, but when 
the argument is universe polymorphic the universes need to be provided.

The standard solution is to use
[Evarutil.new_global : evar_map -> GlobRef.t -> evar_map * constr]
it will create new flexible (as 
https://coq.inria.fr/distrib/current/refman/addendum/universe-polymorphism.html#conversion-and-unification) 
universes to feed to your global.
You then have to pass around the updated evar map to work with it and to 
update the tactic layer (tclEVARS or the like), if you drop it you will 
get undeclared universe errors.

Gaëtan Gilbert

On 10/09/2018 14:28, Christian Doczkal wrote:
> Hi,
> > > - Require Import A B. succeeds
> > > - Require Import B A. fails
> >
> > That sounds like a bug, you can open an issue on github with
> > reproduction instructions and we will look into it.
>
> Unfortunately, that's an internal repository with well over 10K lines,
> and the problem occurs at the end. Should I manage to find a small
> example, I will open an issue.
>
> > > globalization of polymorphic reference <ID> would forget universes.
> >
> > Unfortunately various tactics and commands do not support or badly
> > support universe polymorphism. This error means some function hasn't
> > been adapted. It should probably be an anomaly.
> > Depending on what exactly is failing it may be possible for us to fix
> > it, or it could be beyond our current manpower.
>
> This happens when calling one of our own tactics written in OCaml. So
> how does one have to adapt tactics in order to properly support universe
> polymorphism? (The error occurred while trying to see what happens if I
> make just about everything universe polymorphic, so it may or may not be
> necessary to fix this)
>
> Thanks for the pointers,
> Christian