Skip to content

Instantly share code, notes, and snippets.

Created October 16, 2015 04:08
What would you like to do?
(defun my-pg-preprocessor (coq-sentence)
"Run COQ-SENTENCE through preprocessor and return the result."
(let ((preprocessor (with-current-buffer proof-script-buffer
(expand-file-name "./preprocessor.rb"))))
(insert coq-sentence)
(call-process-region (point-min) (point-max) preprocessor t '(t nil) nil)
(defun my-pg-preprocessor-hook ()
"Preprocess PG's current command."
(setq string (my-pg-preprocessor string)))
(add-hook 'proof-shell-insert-hook #'my-pg-preprocessor-hook)
#!/usr/bin/env ruby
require 'erb'
version = `coqc -v`.match(/version ([^(]*) \(/)[1]
renderer =
puts renderer.result()
Definition proj (n : {n : nat & n >= 2}) : nat :=
match n with
| existT <%= "_" unless version[0..2] == "8.4" %> n _ => n
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment