aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Equality.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2016-08-01 11:49:23 -0700
committerGravatar Jason Gross <jagro@google.com>2016-08-01 11:49:23 -0700
commit331fcc092011215fc7e8e98b6d82435f8327bf8e (patch)
tree9e0eeb6e1d1202788366955ca18e59849569b7fd /src/Util/Equality.v
parent49e1e69975bb250bd05999094d92215cff8acd0c (diff)
Add a tactic to eliminate hprop trivial proofs
Diffstat (limited to 'src/Util/Equality.v')
0 files changed, 0 insertions, 0 deletions