diff options
| author | Pierre-Marie Pédrot | 2014-05-01 17:44:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-01 17:44:51 +0200 |
| commit | 004044b5a377dc36938dc83125cbffb4eae7838c (patch) | |
| tree | ef8b782d52cba8fad16c77b3df92da0a91c2764a /kernel/nativecode.ml | |
| parent | c7b9eebd6e754672d0d57ea6a376bd3d7abf0159 (diff) | |
Allowing the "Declare Instance" command anywhere. This was artificially
restricted to module types, although it was nothing more than a short hand
for Axiom + Existing Instance.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions