diff options
| author | Hugo Herbelin | 2017-02-23 14:34:44 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-02-23 14:52:35 +0100 |
| commit | fedc831df9626a31cd0d26ee6b9e022b67f90c2a (patch) | |
| tree | a2b66571ca95f3460b6818f2f0716e68bfeee133 /kernel/nativecode.ml | |
| parent | 4ddf3ee41eb6e8faaf223041d2bd42d4c62be58d (diff) | |
Fixing a little bug in using the "where" clause for inductive types.
This was not working when the inductive type had implicit parameters.
This could still be improved. E.g. the following still does not work:
Reserved Notation "#".
Inductive I {A:Type} := C : # where "#" := I.
But it should be made working by taking care of adding the mandatory
implicit argument A at the time # is interpreted as [@I _]
(i.e., technically speaking, using expl_impls in interp_notation).
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions