aboutsummaryrefslogtreecommitdiff
path: root/coq/ex/indent_monadic.v
AgeCommit message (Expand)Author
2020-01-19Generic monadic indentation + specifically ext-lib / Compcert + doc.Pierre Courtieu