Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

template-coq should handle primitive projections #38

Open
JasonGross opened this issue Feb 5, 2017 · 0 comments
Open

template-coq should handle primitive projections #38

JasonGross opened this issue Feb 5, 2017 · 0 comments

Comments

@JasonGross
Copy link
Contributor

Consider this unfortunate behavior:

(* -*- coq-prog-args: ("-emacs" "-debug") -*- *)
Require Import Template.Template.
Require Import Template.Ast.
Require Import Coq.Strings.String.
Open Scope string_scope.
Set Primitive Projections.
Set Implicit Arguments.

Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.

Quote Recursively Definition x := @projT1. (* Anomaly: Cannot detype an unfolded primitive projection.. Please report at http://coq.inria.fr/bugs/.
frame @ file "toplevel/vernac.ml", line 242, characters 30-75
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "toplevel/vernac.ml", line 203, characters 6-16
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "stm/stm.ml", line 2828, characters 8-30
frame @ file "stm/stm.ml", line 2298, characters 2-35
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "stm/stm.ml", line 2288, characters 4-48
frame @ file "stm/stm.ml", line 2255, characters 4-100
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "stm/stm.ml", line 885, characters 6-10
frame @ file "stm/stm.ml", line 2140, characters 12-30
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "stm/stm.ml", line 122, characters 15-71
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "lib/flags.ml", line 30, characters 14-17
raise @ unknown
frame @ file "toplevel/vernacentries.ml", line 2232, characters 10-389
frame @ file "lib/flags.ml", line 151, characters 20-45
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "lib/flags.ml", line 30, characters 14-17
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "toplevel/vernacinterp.ml", line 69, characters 4-10
raise @ unknown
raise @ unknown
raise @ unknown
raise @ unknown
raise @ unknown
raise @ unknown
raise @ unknown
raise @ unknown
frame @ file "format.ml", line 1200, characters 6-24
raise @ unknown
frame @ file "interp/constrextern.ml", line 965, characters 2-57
frame @ file "interp/constrextern.ml", line 957, characters 10-69
frame @ file "pretyping/detyping.ml", line 510, characters 7-69
raise @ file "lib/cErrors.ml", line 40, characters 18-39 *)
Definition foo A P (x : @sigT A P) := projT1 x.
Quote Recursively Definition x := foo. (* Anomaly: Uncaught exception Not_found. Please report at http://coq.inria.fr/bugs/.
frame @ file "toplevel/vernac.ml", line 242, characters 30-75
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "toplevel/vernac.ml", line 203, characters 6-16
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "stm/stm.ml", line 2828, characters 8-30
frame @ file "stm/stm.ml", line 2298, characters 2-35
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "stm/stm.ml", line 2288, characters 4-48
frame @ file "stm/stm.ml", line 2255, characters 4-100
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "stm/stm.ml", line 885, characters 6-10
frame @ file "stm/stm.ml", line 2140, characters 12-30
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "stm/stm.ml", line 122, characters 15-71
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "lib/flags.ml", line 30, characters 14-17
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "toplevel/vernacentries.ml", line 2232, characters 10-389
frame @ file "lib/flags.ml", line 151, characters 20-45
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "lib/flags.ml", line 30, characters 14-17
raise @ file "lib/exninfo.ml", line 63, characters 8-15
frame @ file "toplevel/vernacinterp.ml", line 69, characters 4-10
raise @ unknown
raise @ unknown
raise @ unknown
raise @ unknown
raise @ unknown
raise @ unknown
raise @ unknown
raise @ unknown
frame @ file "format.ml", line 1200, characters 6-24
raise @ unknown
frame @ file "interp/constrextern.ml", line 965, characters 2-57
frame @ file "interp/constrextern.ml", line 957, characters 10-69
raise @ unknown
frame @ file "pretyping/detyping.ml", line 515, characters 15-64
frame @ file "pretyping/retyping.ml", line 247, characters 11-44
frame @ file "pretyping/retyping.ml", line 97, characters 19-37
raise @ file "kernel/context.ml", line 187, characters 28-37 *)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant