diff options
| author | Clément Pit--Claudel | 2015-05-02 16:56:16 -0400 |
|---|---|---|
| committer | Pierre Letouzey | 2015-06-22 14:32:19 +0200 |
| commit | 192e683d414ac86d213e2386da40dd7aa5a2fccd (patch) | |
| tree | 811cc345be26ce6e8a779986d28b0c1ddc91e899 /plugins | |
| parent | 5089872d20c9e3089676c9267a6394e99cca5121 (diff) | |
Guard the List.hd call in [Show Intros]
Fix for [Anomaly: Uncaught exception Failure("hd")] after running [Show
Intros] at the end of a proof:
Goal True. trivial. Show Intros.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions