cpitclaudel

(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"))))
    (with-temp-buffer
      (insert coq-sentence)
      (call-process-region (point-min) (point-max) preprocessor t '(t nil) nil)
      (buffer-string))))

(defun my-pg-preprocessor-hook ()