summaryrefslogtreecommitdiff
path: root/test/regress/regress1/nl
diff options
context:
space:
mode:
authoryoni206 <yoni206@users.noreply.github.com>2021-02-25 12:36:05 -0800
committerGitHub <noreply@github.com>2021-02-25 14:36:05 -0600
commit6a4b16c643d71c9318042ba7b9d42af71c58ac2f (patch)
tree0092464e48a09bd71eff04b1d4d44cc3fac31bc0 /test/regress/regress1/nl
parent9a58e63237298be0c81fe88096f65d935be97e82 (diff)
Datatypes lemmas: share only external types (#5997)
Forcing lemmas in datatypes used to be done only for external types. This was changed to consider all types, which is not needed. This PR brings back the restriction to external types.
Diffstat (limited to 'test/regress/regress1/nl')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback