diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-24 15:34:12 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:07 +0100 |
commit | 77ef9a400cd570e0857a45c015bca0308e2a0eff (patch) | |
tree | f17d2698af2f1e54b65da561ed7175a293a637b1 /vernac/metasyntax.ml | |
parent | 5806b0476a1ac9b903503641cc3e2997d3e8d960 (diff) |
User-level support for Gonthier-Ssreflect's "if t then pat then u else v".
Diffstat (limited to 'vernac/metasyntax.ml')
0 files changed, 0 insertions, 0 deletions