Preprocessing commands in Proof-General (inspired from http://coq-blog.clarus.me/why-and-how-to-write-code-compatible-with-many-coq-versions.html)

pg-plugin.el

(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 ()
  "Preprocess PG's current command."
  (setq string (my-pg-preprocessor string)))

(add-hook 'proof-shell-insert-hook #'my-pg-preprocessor-hook)

preprocessor.rb

#!/usr/bin/env ruby
require 'erb'

version = `coqc -v`.match(/version ([^(]*) \(/)[1]
renderer = ERB.new(STDIN.read)
puts renderer.result()

test.v

Definition proj (n : {n : nat & n >= 2}) : nat :=
  match n with
  | existT <%= "_" unless version[0..2] == "8.4" %> n _ => n
  end.