Binary logical relations library for the Coq proof assistant
Coq HTML
Latest commit 1a7b900 Feb 23, 2017 @jeremie-koenig jeremie-koenig Generalize the [preorder] tactic into [rgraph]
We no longer require the relation to be reflexive, and we make use of
symmetry when available.