summaryrefslogtreecommitdiff
path: root/test-suite/output
ModeNameSize
-rw-r--r--Arith.out71logplain
-rw-r--r--Arith.v45logplain
-rw-r--r--Cases.out196logplain
-rw-r--r--Cases.v101logplain
-rw-r--r--Coercions.out38logplain
-rw-r--r--Coercions.v245logplain
-rw-r--r--Fixpoint.v166logplain
-rw-r--r--Implicit.out125logplain
-rw-r--r--Implicit.v586logplain
-rw-r--r--InitSyntax.out179logplain
-rw-r--r--InitSyntax.v93logplain
-rw-r--r--Intuition.out87logplain
-rw-r--r--Intuition.v100logplain
-rw-r--r--Nametab.out586logplain
-rw-r--r--Nametab.v779logplain
-rw-r--r--RealSyntax.out33logplain
-rw-r--r--RealSyntax.v44logplain
-rw-r--r--Remark2.out30logplain
-rw-r--r--Remark2.v94logplain
-rw-r--r--Sum.out87logplain
-rw-r--r--Sum.v75logplain
-rw-r--r--TranspModtype.out92logplain
-rw-r--r--TranspModtype.v363logplain
-rw-r--r--ZSyntax.out518logplain
-rw-r--r--ZSyntax.v488logplain
-rw-r--r--implicits.out103logplain
-rw-r--r--implicits.v460logplain