diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 10:24:18 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 10:24:18 +0100 |
| commit | fd852113ea205720a9394c27989acaac408f7643 (patch) | |
| tree | f3cb2d7b11c3bb161139ac81232c343c980c45e0 /configure.ml | |
| parent | 49dd2bddc03ce64707cb93d450127152ad6eece6 (diff) | |
| parent | e7bf157c6af0d7f65b0611f7dfa9c00d5e1e7a83 (diff) | |
Merge PR #6328: Fix #6313: lost goals in nested ltac in refine
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions