metacoq icon indicating copy to clipboard operation
metacoq copied to clipboard

`tmQuoteModule` generates many anomalies

Open JasonGross opened this issue 2 years ago • 0 comments

From MetaCoq.Utils Require Import bytestring.
From MetaCoq.Template Require Import Loader TemplateMonad.
From Coq Require Import MSetInterface MSetFacts.
Open Scope bs.
Locate Module Nop. (* Module Type Coq.Structures.Equalities.Nop *)
MetaCoq Run (tmQuoteModule "Nop").
(* Error: Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.
 *)
MetaCoq Run (tmQuoteModule "Coq.Init").
(* Error: Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.
 *)
MetaCoq Run (tmQuoteModule "a").
(* Error: Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.
*)
MetaCoq Run (tmQuoteModule "").
(* Error: Anomaly "Uncaught exception Failure("split_dirpath")."
Please report at http://coq.inria.fr/bugs/.
*)
MetaCoq Run (tmQuoteModule "DecidableType").
(* Error:
<in exception printer>:<original exception:Anomaly
                                           "File "vernac/himsg.ml", line 945, characters 13-19: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
*)

JasonGross avatar Feb 14 '23 21:02 JasonGross