diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-03 16:50:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-03 16:50:40 +0200 |
| commit | b0e8bf149a9c620f2e2bd25f586fb41ee71aae0d (patch) | |
| tree | edcec459b613857728557f93c7b73ad7900ed0c3 /API | |
| parent | a2a98a4015311af83edcf8fc87aa30a5318bead8 (diff) | |
[tactics] Fix summary registration of global hint variable.
It looks like `Class_tactics` forgot to register a couple of global
variables with the summary, thus creating problems on backtracking.
Fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5578
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions