Closed DeLectionnes closed 7 months ago
In 8.18, MetaCoq Run sends an anomaly if you Run a piece of code that is not typed correctly, and that the Coq typechecker rejects.
In 8.16, it only sends an error, not an anomaly.
This happens with the version 1.2.1+8.18 installed via opam.
From MetaCoq.Utils Require Import utils. From MetaCoq.Template Require Import All. Import MCMonadNotation. (*Exemple with a typing error*) Definition ident_term (a : term) : term := a. Definition quote_inductive {X}(inductive:X): TemplateMonad _ := quote <- tmQuote inductive;; tmReturn quote. Inductive tm : Set := . Definition d1 : TemplateMonad unit. Fail refine ( quote <- quote_inductive tm;; constructor <- ident_term quote;; tmPrint constructor) . (*The command has indeed failed with message: In environment quote : term Unable to unify "term" with "TemplateMonad ?Goal2". (while solving unification constraints, see flag "Solve Unification Constraints")*) Abort. Fail MetaCoq Run( quote <- quote_inductive tm;; constructor <- ident_term quote;; tmPrint constructor) . (*Error: Anomaly "File "kernel/constr.ml", line 1485, characters 26-32: Assertion failed." Please report at http://coq.inria.fr/bugs/.*) ``
Fixed in #1068 and released in 1.3.1 versions (soon in opam)
In 8.18, MetaCoq Run sends an anomaly if you Run a piece of code that is not typed correctly, and that the Coq typechecker rejects.
In 8.16, it only sends an error, not an anomaly.
This happens with the version 1.2.1+8.18 installed via opam.