aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenvtac.mli
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-07-21 13:43:31 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-03-01 12:05:39 +0100
commit711b9d8cdf6e25690d247d9e8c49f005527e64e2 (patch)
tree5a19ec52e7a510a456195d3814958abc33e47f73 /proofs/clenvtac.mli
parentf726e860917b56abc94f21d9d5add7594d23bb6d (diff)
Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".
Noticed by Sigurd Schneider.
Diffstat (limited to 'proofs/clenvtac.mli')
0 files changed, 0 insertions, 0 deletions