Anomaly: Uncaught exception Reify.TermReify.NotSupported(_). Please report at http://coq.inria.fr/bugs/.

gmalecha / template-coq

Reflection library for Coq

MIT License

12 stars 0 forks source link

Anomaly: Uncaught exception Reify.TermReify.NotSupported(_). Please report at http://coq.inria.fr/bugs/. #39

Open JasonGross opened 7 years ago

JasonGross commented 7 years ago

Require Import Template.Ast.
Require Import Template.Template.
Require Import Coq.Strings.String.
Open Scope string_scope.

Quote Definition qfoo := (fix foo (n : nat) := 0).
Make Definition foo' := qfoo.

gmalecha commented 7 years ago

I think this is due to the fact that Make Definition is not really completely implemented.

aa755 commented 7 years ago

As a workaround, I would try Make Definition foo' := ltac:(let t:= eval compute in qfoo in exact t). I believe this problem is fixed in some branches.