aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-09-27 20:02:54 +0200
committerMatthieu Sozeau2014-09-27 20:41:05 +0200
commit3ca949d4069308cf71c8f22b8dfc89e95a3834c1 (patch)
treee62c966cf36841deeba474bd4b722881ed9f39b2 /plugins
parentb6e39ade125862ba41ca17b06b8e35726b9b0d7d (diff)
Remove auto's use of dummy goal, use the proper sigma for pattern_of_constr.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions