aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorMatthieu Sozeau2017-01-24 17:24:39 +0100
committerMatthieu Sozeau2018-03-08 07:56:59 -0300
commit7ceed3c76e5ac752321827300f80ee974acbb54c (patch)
tree3c9198c9405c3d2d0df474a0a1c79722414b3841 /dev/base_include
parente3124e098ef8170dac2b348b91757a7034bc4999 (diff)
Fix SR breakage due to allowing fixpoints on non-rec values
We limit fixpoints to Finite inductive types, so that BiFinite inductives (non-recursive records) are excluded from fixpoint construction. This is a regression in the sense that e.g. fixpoints on unit records were allowed before. Primitive records with eta-conversion are included in the BiFinite types. Fix deprecation Fix error message, the inductive type needs to be recursive for fix to work
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions