diff options
| author | Pierre-Marie Pédrot | 2020-03-05 15:14:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-08 15:31:27 +0100 |
| commit | 4481b95f6f89acd7013b16a345d379dc44d67705 (patch) | |
| tree | cd1d0f1c59a3a27aa1fd777797834fc15ac71a38 /kernel/environ.ml | |
| parent | 6143ac9f9307b2f6863cca019a66cdcbfd52d7ce (diff) | |
Template polymorphism is now a property of the inductive block.
For an inductive block to be template, all its components must also
be. This is probably fixing a few soundness bugs in the process, but I
do not want to think too much about it.
Diffstat (limited to 'kernel/environ.ml')
0 files changed, 0 insertions, 0 deletions