The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

On Wed, Jul 6, 2016 at 1:46 PM, Matthieu Sozeau <mattam AT mattam.org> wrote:

Hi, 

  this is an indication that universes are not properly registered (or more rarely that you're giving the conversion function ill-typed terms or terms of different types). You are probably not threading the evar_map correctly in your tactic, or not calling the necessary Typing functions to compute universe constraints. There is documentation in dev/doc/univpoly.txt and the following slides that should answer your questions: 

https://coq.inria.fr/cocorico/CoqImplementorsWorkshop/CoqIW2016

Great!

 

  8.6 will have a GADT based interface that can enforce this by typing :) Also, this may be more appropriate for coqdev.

You're right.

Best,

Beta

 

Best,

-- Matthieu

On Wed, Jul 6, 2016 at 1:23 PM Beta Ziliani <beta AT mpi-sws.org> wrote:

This is primarly targeted to the devs in the list.

I have a tactic that produces a term that, apparently, makes some Reductionops function fail with the error message "Conversion raised an anomaly". Oddly enough, if I copy the (Set Printing All) term, and pose it, it works, so the term is well constructed (modulo universes). Does anyone have an idea what can be happening, or how can I get further information on the issue?

Thanks,

Beta