diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-02 14:36:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-03 11:00:17 +0100 |
| commit | fbb0d3151820517dee2f8e467435a6f045efbee0 (patch) | |
| tree | 18a1f2402cc27b3304c9cb3306379bf8afd3a2e1 /test-suite/bugs/closed/HoTT_coq_077.v | |
| parent | b5990eb632c2a959b7a86ea9c7e4970505e976a1 (diff) | |
Removing the use of tacticIn in Tauto.
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_077.v')
0 files changed, 0 insertions, 0 deletions