Respect the COQBIN environment variables

This allows us to specify a non-system Coq to build with, by, e.g.,
setting COQBIN=~/.local/coq/coq-trunk/bin/.
Require Import Omega

This is required in trunk to use the [omega] tactic.
Asymmetric Patterns
Avoid name clash
ml reification for trunk
New proof engine compatibility
NPeano -> PeanoNat.Nat
You cannot implicitly used cleared variable anymore
alpha renaiming and consequence of tactics improvements
Minor changes