aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.ml
diff options
context:
space:
mode:
authorSimonBoulier2018-11-05 11:18:08 +0100
committerSimonBoulier2019-08-16 11:43:51 +0200
commitbc4560fa6c88aadcb2ee8312a950a7ce17fc33ee (patch)
treeae0d5cf3ee6c859d833c7168fe9d21a8fa3b3abd /printing/printer.ml
parentd72acd6f1a5abb8066b6922e5e972fa17b215591 (diff)
Split the [check_guarded] typing_flag into [check_guarded] (for (co)fixpoints) and [check_positive] (for (co)inductive types).
Diffstat (limited to 'printing/printer.ml')
0 files changed, 0 insertions, 0 deletions