aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
ModeNameSize
-rw-r--r--Arguments.out3896logplain
-rw-r--r--Arguments.v1468logplain
-rw-r--r--ArgumentsScope.out1539logplain
-rw-r--r--ArgumentsScope.v535logplain
-rw-r--r--Arguments_renaming.out4417logplain
-rw-r--r--Arguments_renaming.v1018logplain
-rw-r--r--Cases.out1743logplain
-rw-r--r--Cases.v1607logplain
-rw-r--r--Coercions.out108logplain
-rw-r--r--Coercions.v651logplain
-rw-r--r--Errors.out326logplain
-rw-r--r--Errors.v359logplain
-rw-r--r--Existentials.out234logplain
-rw-r--r--Existentials.v225logplain
-rw-r--r--Extraction_matchs_2413.out1058logplain
-rw-r--r--Extraction_matchs_2413.v2742logplain
-rw-r--r--Fixpoint.out463logplain
-rw-r--r--Fixpoint.v1048logplain
-rw-r--r--Implicit.out422logplain
-rw-r--r--Implicit.v1267logplain
-rw-r--r--InitSyntax.out393logplain
-rw-r--r--InitSyntax.v111logplain
-rw-r--r--Intuition.out86logplain
-rw-r--r--Intuition.v121logplain
-rw-r--r--Match_subterm.out36logplain
-rw-r--r--Match_subterm.v86logplain
-rw-r--r--Nametab.out1672logplain
-rw-r--r--Nametab.v917logplain
-rw-r--r--Naming.out1659logplain
-rw-r--r--Naming.v1957logplain
-rw-r--r--Notations.out3658logplain
-rw-r--r--Notations.v8518logplain
-rw-r--r--Notations2.out1199logplain
-rw-r--r--Notations2.v3163logplain
-rw-r--r--NumbersSyntax.out950logplain
-rw-r--r--NumbersSyntax.v1351logplain
-rw-r--r--PrintAssumptions.out844logplain
-rw-r--r--PrintAssumptions.v2422logplain
-rw-r--r--PrintInfos.out4472logplain
-rw-r--r--PrintInfos.v682logplain
-rw-r--r--Quote.out972logplain
-rw-r--r--Quote.v911logplain
-rw-r--r--RealSyntax.out31logplain
-rw-r--r--RealSyntax.v49logplain
-rw-r--r--Record.out212logplain
-rw-r--r--Record.v385logplain
-rw-r--r--Search.out1392logplain
-rw-r--r--Search.v155logplain
-rw-r--r--SearchPattern.out2152logplain
-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.out128logplain
-rw-r--r--Tactics.v357logplain
-rw-r--r--TranspModtype.out229logplain
-rw-r--r--TranspModtype.v385logplain
-rw-r--r--ZSyntax.out578logplain
-rw-r--r--ZSyntax.v558logplain
-rw-r--r--inference.out588logplain
-rw-r--r--inference.v856logplain
-rw-r--r--names.out178logplain
-rw-r--r--names.v132logplain
-rw-r--r--reduction.out44logplain
-rw-r--r--reduction.v279logplain
-rw-r--r--rewrite-2172.out101logplain
-rw-r--r--rewrite-2172.v734logplain
-rw-r--r--set.out279logplain
-rw-r--r--set.v154logplain
-rw-r--r--simpl.out201logplain
-rw-r--r--simpl.v154logplain