aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
ModeNameSize
-rw-r--r--Cases.out217logplain
-rw-r--r--Cases.out8357logplain
-rw-r--r--Cases.v101logplain
-rw-r--r--Cases.v8112logplain
-rw-r--r--Coercions.out81logplain
-rw-r--r--Coercions.out890logplain
-rw-r--r--Coercions.v390logplain
-rw-r--r--Coercions.v8412logplain
-rw-r--r--Fixpoint.out200logplain
-rw-r--r--Fixpoint.out8395logplain
-rw-r--r--Fixpoint.v166logplain
-rw-r--r--Fixpoint.v8387logplain
-rw-r--r--Implicit.out232logplain
-rw-r--r--Implicit.out8276logplain
-rw-r--r--Implicit.v586logplain
-rw-r--r--Implicit.v8647logplain
-rw-r--r--InitSyntax.out304logplain
-rw-r--r--InitSyntax.out8393logplain
-rw-r--r--InitSyntax.v93logplain
-rw-r--r--InitSyntax.v8110logplain
-rw-r--r--Intuition.out87logplain
-rw-r--r--Intuition.out891logplain
-rw-r--r--Intuition.v100logplain
-rw-r--r--Intuition.v8120logplain
-rw-r--r--Nametab.out8928logplain
-rw-r--r--Nametab.v890logplain
-rw-r--r--Notations.out8350logplain
-rw-r--r--Notations.v8567logplain
-rw-r--r--RealSyntax.out33logplain
-rw-r--r--RealSyntax.out831logplain
-rw-r--r--RealSyntax.v44logplain
-rw-r--r--RealSyntax.v848logplain
-rw-r--r--Sum.out95logplain
-rw-r--r--Sum.out899logplain
-rw-r--r--Sum.v75logplain
-rw-r--r--Sum.v892logplain
-rw-r--r--TranspModtype.out892logplain
-rw-r--r--TranspModtype.v8384logplain
-rw-r--r--ZSyntax.out528logplain
-rw-r--r--ZSyntax.out8586logplain
-rw-r--r--ZSyntax.v488logplain
-rw-r--r--ZSyntax.v8557logplain