mit-plv/fiat-crypto

par nsatz unshelve anomalies

andres-erbsen opened this issue · 2 comments

andres-erbsen commented 
Require Import Crypto.Algebra.Nsatz BinInt.

Goal  id (True) -> Z0 = Z0 /\ Z0 = Z0.
Proof.
  split.
  1:shelve.
  Time par: abstract Nsatz.nsatz.
  Unshelve.
  Time par: abstract Nsatz.nsatz.
  (*
Anomaly
"in Univ.repr: Universe Top.tacticworker:0.1 undefined."
Please report at http://coq.inria.fr/bugs/.
   *)

Goal  id (True) -> Z0 = Z0 /\ Z0 = Z0.
Proof.
  split.
  1:shelve.
  Time par: Nsatz.nsatz.
  Unshelve.
  Time par: Nsatz.nsatz.
  (*
Anomaly "Uncaught exception AcyclicGraph.Make(Point).AlreadyDeclared."
Please report at http://coq.inria.fr/bugs/. (for goal 1)

🤷‍♂️

JasonGross commented

Run through bug minimizer and report on coq/coq?