summaryrefslogtreecommitdiff
path: root/test-suite/output
ModeNameSize
-rw-r--r--Cases.out281logplain
-rw-r--r--Cases.v113logplain
-rw-r--r--Coercions.out90logplain
-rw-r--r--Coercions.v413logplain
-rw-r--r--Fixpoint.out395logplain
-rw-r--r--Fixpoint.v388logplain
-rw-r--r--Implicit.out276logplain
-rw-r--r--Implicit.v648logplain
-rw-r--r--InitSyntax.out395logplain
-rw-r--r--InitSyntax.v111logplain
-rw-r--r--Intuition.out91logplain
-rw-r--r--Intuition.v121logplain
-rw-r--r--Nametab.out1096logplain
-rw-r--r--Nametab.v906logplain
-rw-r--r--Notations.out873logplain
-rw-r--r--Notations.v3420logplain
-rw-r--r--RealSyntax.out31logplain
-rw-r--r--RealSyntax.v49logplain
-rw-r--r--Sum.out99logplain
-rw-r--r--Sum.v93logplain
-rw-r--r--Tactics.out132logplain
-rw-r--r--Tactics.v488logplain
-rw-r--r--TranspModtype.out92logplain
-rw-r--r--TranspModtype.v385logplain
-rw-r--r--ZSyntax.out586logplain
-rw-r--r--ZSyntax.v558logplain