aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-02-07 17:10:49 +0100
committerPierre-Marie Pédrot2020-03-08 15:31:27 +0100
commit6143ac9f9307b2f6863cca019a66cdcbfd52d7ce (patch)
tree0544010e738d07d6c4e87224c27dfa07e6b894eb /checker
parentdbd3a4c4213b3d56908a8387de93e27aaec501a4 (diff)
Do not hardcode specific handling of Prop levels in template poly.
We also factorize a few checks by returning an option when looking for a potentially template universe.
Diffstat (limited to 'checker')
0 files changed, 0 insertions, 0 deletions