summaryrefslogtreecommitdiff
path: root/test-suite/output
ModeNameSize
-rw-r--r--ArgumentsScope.out1083logplain
-rw-r--r--ArgumentsScope.v535logplain
-rw-r--r--Cases.out916logplain
-rw-r--r--Cases.v839logplain
-rw-r--r--Coercions.out108logplain
-rw-r--r--Coercions.v651logplain
-rw-r--r--Existentials.out48logplain
-rw-r--r--Existentials.v225logplain
-rw-r--r--Extraction_matchs_2413.out1114logplain
-rw-r--r--Extraction_matchs_2413.v2732logplain
-rw-r--r--Fixpoint.out612logplain
-rw-r--r--Fixpoint.v898logplain
-rw-r--r--Implicit.out344logplain
-rw-r--r--Implicit.v947logplain
-rw-r--r--InitSyntax.out382logplain
-rw-r--r--InitSyntax.v111logplain
-rw-r--r--Intuition.out91logplain
-rw-r--r--Intuition.v121logplain
-rw-r--r--Match_subterm.out25logplain
-rw-r--r--Match_subterm.v86logplain
-rw-r--r--Nametab.out1114logplain
-rw-r--r--Nametab.v917logplain
-rw-r--r--Naming.out1789logplain
-rw-r--r--Naming.v1957logplain
-rw-r--r--Notations.out3316logplain
-rw-r--r--Notations.v7455logplain
-rw-r--r--Notations2.out618logplain
-rw-r--r--Notations2.v2101logplain
-rw-r--r--NumbersSyntax.out965logplain
-rw-r--r--NumbersSyntax.v1351logplain
-rw-r--r--Quote.out972logplain
-rw-r--r--Quote.v911logplain
-rw-r--r--RealSyntax.out31logplain
-rw-r--r--RealSyntax.v49logplain
-rw-r--r--Search.out607logplain
-rw-r--r--Search.v143logplain
-rw-r--r--SearchPattern.out697logplain
-rw-r--r--SearchPattern.v408logplain
-rw-r--r--SearchRewrite.out72logplain
-rw-r--r--SearchRewrite.v118logplain
-rw-r--r--Sum.out99logplain
-rw-r--r--Sum.v93logplain
-rw-r--r--Tactics.out132logplain
-rw-r--r--Tactics.v488logplain
-rw-r--r--TranspModtype.out89logplain
-rw-r--r--TranspModtype.v385logplain
-rw-r--r--ZSyntax.out571logplain
-rw-r--r--ZSyntax.v558logplain
-rw-r--r--reduction.out44logplain
-rw-r--r--reduction.v278logplain
-rw-r--r--set.out315logplain
-rw-r--r--set.v154logplain
-rw-r--r--simpl.out201logplain
-rw-r--r--simpl.v148logplain