aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-12-23 17:32:23 +0100
committerPierre-Marie Pédrot2015-12-23 17:41:12 +0100
commit74ebc8b3c20a41f17244d3ab13f984ede2e201e3 (patch)
treeef21a34271d575aedf59a8fe5c396fd41a698a09 /plugins/firstorder
parent8c684847844b25bd4ce071867fb480c9caa8cb62 (diff)
Partial backtrack on commit 20641795624.
The parsing rules were broken and disallowed tactic replacement of the form Ltac ident ::= expr.
Diffstat (limited to 'plugins/firstorder')
0 files changed, 0 insertions, 0 deletions