metacoq
metacoq copied to clipboard
`tmQuoteModule` generates many anomalies
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/.
*)