aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorHugo Herbelin2018-09-26 11:41:05 +0200
committerHugo Herbelin2018-09-26 11:41:05 +0200
commitbebd946584b33a5e263393bd88e8571cd5fa5af2 (patch)
tree514fd72bd77f76b1d4e11783160c606a776330e3 /dev
parentccb701d78394a108daf25e62d40ba059aa3fce62 (diff)
Fix for Coq PR#8554 (term builder for tactic "change" takes an environment).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions