diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-17 01:14:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-17 01:15:32 +0200 |
| commit | beb3acd2fd3831404f0be2da61d3f28e210e8349 (patch) | |
| tree | ac61acef6eef5ccf9c446b486c9443c915b83af1 /vernac/topfmt.ml | |
| parent | 0147ae6ba6db24d4f9b29ff477d374a6abb103dd (diff) | |
Add a test for bug #5321: clearbody breaks typing of goal.
The bug has been solved as a side-effect of the EConstr branch.
Diffstat (limited to 'vernac/topfmt.ml')
0 files changed, 0 insertions, 0 deletions