diff options
| author | Emilio Jesus Gallego Arias | 2016-09-20 12:35:11 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-09-20 12:35:11 +0200 |
| commit | 3bf6fbc4d339545b0eace0689adfec048f1c8530 (patch) | |
| tree | c1ff2fad749c8b5e813cdbc34683bcfb1bd0ff7e /mathcomp/ssreflect/plugin | |
| parent | b7796bb785b9d37e5b6648489d5c28e85df9d90d (diff) | |
[field] Remove unnecessary `Program Definition`
Simple `Definition` should work fine here.
This avoids the problem:
`Error: Library Coq.Program.Tactics has to be required first.`
in math-comp versions that depends on a minimal (or no) Coq stdlib.
Tested on 8.5/8.6
Diffstat (limited to 'mathcomp/ssreflect/plugin')
0 files changed, 0 insertions, 0 deletions