Debugger entered--Lisp error: (arith-error)
  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)
  ad-Orig-font-lock-fontify-keywords-region(1 363 nil)
  (setq ad-return-value (ad-Orig-font-lock-fontify-keywords-region beg end loudly))
  (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)
  font-lock-fontify-keywords-region(1 363 nil)
  font-lock-default-fontify-region(1 363 nil)
  font-lock-fontify-region(1 363)
  run-hook-with-args(font-lock-fontify-region 1 363)
  byte-code("ÂÃ	#‡" [start next run-hook-with-args jit-lock-functions] 4)
  jit-lock-fontify-now(1 501)
  jit-lock-function(1)
  pos-visible-in-window-p(362 #<window 12 on *response*>)
  proof-display-and-keep-buffer(#<buffer *response*>)
  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")
  proof-shell-handle-delayed-output()
  proof-shell-filter-manage-output(8242 8604)
  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>")
  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>")
  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>")