| 1 | Debugger entered--Lisp error: (arith-error) |
|---|
| 2 | re-search-forward("\\(\\(?:\\_<Axiom\\_>\\)\\|\\(?:\\_<Global\\s-+Variable\\_>\\)\\|\\(?:\\_<Global\\s-+Variables\\_>\\)\\|\\(?:\\_<Hint\\s-+Constructors\\_>\\)\\|\\(?:\\_<Hint\\s-+Extern\\_>\\)\\|\\(?:\\_<Hint\\s-+Immediate\\_>\\)\\|\\(?:\\_<Hint\\s-+Resolve\\_>\\)\\|\\(?:\\_<Hint\\s-+Rewrite\\_>\\)\\|\\(?:\\_<\\_>\\)\\|\\(?:\\_<Hint\\s-+Unfold\\_>\\)\\|\\(?:\\_<Existing\\s-+Instance\\_>\\)\\|\\(?:\\_<Hypothesis\\_>\\)\\|\\(?:\\_<Hypotheses\\_>\\)\\|\\(?:\\_<Parameter\\_>\\)\\|\\(?:\\_<Parameters\\_>\\)\\|\\(?:\\_<Conjecture\\_>\\)\\|\\(?:\\_<Variable\\_>\\)\\|\\(?:\\_<Variables\\_>\\)\\|\\(?:\\_<Coercion\\_>\\)\\)\\s-+\\(\\(\\w\\(\\w\\|\\s_\\)*\\)\\(\\s-* \\s-*\\(\\w\\(\\w\\|\\s_\\)*\\)\\)*\\)\\s-*:" 363 t) |
|---|
| 3 | ad-Orig-font-lock-fontify-keywords-region(1 363 nil) |
|---|
| 4 | (setq ad-return-value (ad-Orig-font-lock-fontify-keywords-region beg end loudly)) |
|---|
| 5 | (let (ad-return-value) (when (and proof-buffer-type ...) (funcall ... beg end loudly)) (setq ad-return-value (ad-Orig-font-lock-fontify-keywords-region beg end loudly)) ad-return-value) |
|---|
| 6 | font-lock-fontify-keywords-region(1 363 nil) |
|---|
| 7 | font-lock-default-fontify-region(1 363 nil) |
|---|
| 8 | font-lock-fontify-region(1 363) |
|---|
| 9 | run-hook-with-args(font-lock-fontify-region 1 363) |
|---|
| 10 | byte-code("ÂÃ #" [start next run-hook-with-args jit-lock-functions] 4) |
|---|
| 11 | jit-lock-fontify-now(1 501) |
|---|
| 12 | jit-lock-function(1) |
|---|
| 13 | pos-visible-in-window-p(362 #<window 12 on *response*>) |
|---|
| 14 | proof-display-and-keep-buffer(#<buffer *response*>) |
|---|
| 15 | pg-response-display("Module Type T = Sig\n Parameter p1\n Parameter p2\n Parameter p3\n Parameter p4\n Parameter p5\n Parameter p6\n Parameter p7\n Parameter p8\n Parameter p9\n End\n\nFinished transaction in 0. secs (0.u,0.s)\n") |
|---|
| 16 | proof-shell-handle-delayed-output() |
|---|
| 17 | proof-shell-filter-manage-output(8242 8604) |
|---|
| 18 | proof-shell-filter("Module Type T = Sig\n Parameter p1\n Parameter p2\n Parameter p3\n Parameter p4\n Parameter p5\n Parameter p6\n Parameter p7\n Parameter p8\n Parameter p9\n End\n\nFinished transaction in 0. secs (0.u,0.s)\n\n<prompt>Coq < 52 || 0 < </prompt>") |
|---|
| 19 | run-hook-with-args(proof-shell-filter "Module Type T = Sig\n Parameter p1\n Parameter p2\n Parameter p3\n Parameter p4\n Parameter p5\n Parameter p6\n Parameter p7\n Parameter p8\n Parameter p9\n End\n\nFinished transaction in 0. secs (0.u,0.s)\n\n<prompt>Coq < 52 || 0 < </prompt>") |
|---|
| 20 | scomint-output-filter(#<process coq> "Module Type T = Sig\n Parameter p1\n Parameter p2\n Parameter p3\n Parameter p4\n Parameter p5\n Parameter p6\n Parameter p7\n Parameter p8\n Parameter p9\n End\n\nFinished transaction in 0. secs (0.u,0.s)\n\n<prompt>Coq < 52 || 0 < </prompt>") |
|---|
