aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2016-01-27 17:55:02 +0100
committerGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2016-01-27 17:55:02 +0100
commit626013259652e208ce99c84463e05ce22e62484a (patch)
tree1c202419e91b62dd5c43a2e12fc38c35c5ba6883 /generic
parentd35b46774617b44776730adf9d8ea4807a75e8a2 (diff)
Fixed recent coq syntax change (tac !H become tac (H)).
Diffstat (limited to 'generic')
0 files changed, 0 insertions, 0 deletions