coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] universe inconsistency on import

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] universe inconsistency on import
Date: Fri, 29 Nov 2019 16:56:52 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vzaliva AT cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-io1-f49.google.com
Ironport-phdr: 9a23:OxMBGxZEljP+9du0F9+t8VX/LSx+4OfEezUN459isYplN5qZoMi4bnLW6fgltlLVR4KTs6sC17ON9fm/ASdavN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vIhi6txjdu8sKjYdtNKo8ygbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDM/7WrZiNF/jLhDrR2upxJxzY3abpyLOvViZa7SZ88WSHBbU8pNSyBMAIWxZJYPAeobOuZYqpHwqFQUohSjBAmsAf7kxTxSiX/y3K06zf4uGhzB0Qw+HtMBqnDUrNTrNKgISu260KzIzSjZY/xIxDj99ZHFfxY8qv+CWrJwdNDeyUgpFw7diFWfs4nlMC2M2usRtGiU9fZvVeK1h2E7rAFxpz6izdovhInRno8Z1EzI+CFjzIs2JdC0UlN3bN+lHZdKuCyXM417Sd44TW5yoiY10LgGtIa7fCcUzJQnwAbSa/mdfIiJ5hLvTeeRITBliH58drKyiBK//VKvyu37Ucm031JKoTRfntbQsXAN0gTf6smBSvRj4keswSiD2xzX5+1eIk05lbDXJ4Mgz7MxjJYevkDOEjfzmErsja+Wcksk+vKv6+TierjmuIWTOJJ1igH7KKgvm9awAeA5MggQRWeW4uq926P4/U3lWrlFkvg2krTDvJ/EOMsbu7a1AxVJ3YY79xa/EzCm3cwEknkANVJJYQ6Ij4z0O17VO/34Fve+g1G0kDhx3fzGP7vhAo/MLnfZirvhc6x9uAZgz184yska7JZJAJkAJujyUwn/ro/2FBg8ZjK9z+fiQOd00oIAUCrbHL2QNKLMuHeD4/9pLuWRMtxG8A3hIuQosqa9xUQynkUQKPHwgMknLUugF/EjGH23JHrhhtBbTDUPtws6Ce3t0RiMDW8VaHG1UKYxoDo8DdD+VNuRdsWWmLWEmRyDMNhOfGkXWFuJDDHle5jWA65dOhLXGddol3k/bZbkToYg0R+0swqjl+h4I/HIvCYdqNTu2MUnvuA=

I have `Require Import` which fails with the "universe inconsistency" error. There is no more detail besides this message. Any hints on how one can debug this?

Vadim

Vadim Zaliva

A button for name playback in email signature

CMU ECE Ph.D. candidate

Mobile/Signal/WhatsApp: +1(510)220-1060

[Coq-Club] universe inconsistency on import, Vadim Zaliva, 11/30/2019
- Re: [Coq-Club] universe inconsistency on import, Brett Gilio, 11/30/2019
  - Re: [Coq-Club] universe inconsistency on import, Jason Gross, 11/30/2019
    - Re: [Coq-Club] universe inconsistency on import, Christian Doczkal, 11/30/2019