summaryrefslogtreecommitdiff
path: root/test-suite/output
ModeNameSize
-rw-r--r--Arguments.out3463logplain
-rw-r--r--Arguments.v1470logplain
-rw-r--r--ArgumentsScope.out1083logplain
-rw-r--r--ArgumentsScope.v560logplain
-rw-r--r--Arguments_renaming.out4378logplain
-rw-r--r--Arguments_renaming.v1049logplain
-rw-r--r--Binder.out168logplain
-rw-r--r--Binder.v134logplain
-rw-r--r--Cases.out2014logplain
-rw-r--r--Cases.v2420logplain
-rw-r--r--Coercions.out108logplain
-rw-r--r--Coercions.v651logplain
-rw-r--r--Errors.out458logplain
-rw-r--r--Errors.v548logplain
-rw-r--r--Existentials.out237logplain
-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.out391logplain
-rw-r--r--Implicit.v1267logplain
-rw-r--r--Inductive.out143logplain
-rw-r--r--Inductive.v94logplain
-rw-r--r--InitSyntax.out433logplain
-rw-r--r--InitSyntax.v111logplain
-rw-r--r--Intuition.out85logplain
-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.out1639logplain
-rw-r--r--Naming.v1957logplain
-rw-r--r--Notations.out3661logplain
-rw-r--r--Notations.v8482logplain
-rw-r--r--Notations2.out1594logplain
-rw-r--r--Notations2.v4183logplain
-rw-r--r--Notations3.out3528logplain
-rw-r--r--Notations3.v5247logplain
-rw-r--r--NumbersSyntax.out950logplain
-rw-r--r--NumbersSyntax.v1351logplain
-rw-r--r--PatternsInBinders.out1168logplain
-rw-r--r--PatternsInBinders.v1613logplain
-rw-r--r--PrintAssumptions.out574logplain
-rw-r--r--PrintAssumptions.v2582logplain
-rw-r--r--PrintInfos.out3366logplain
-rw-r--r--PrintInfos.v947logplain
-rw-r--r--PrintModule.out146logplain
-rw-r--r--PrintModule.v567logplain
-rw-r--r--Quote.out963logplain
-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.out4123logplain
-rw-r--r--Search.v1122logplain
-rw-r--r--SearchHead.out1411logplain
-rw-r--r--SearchHead.v460logplain
-rw-r--r--SearchPattern.out2215logplain
-rw-r--r--SearchPattern.v1002logplain
-rw-r--r--SearchRewrite.out120logplain
-rw-r--r--SearchRewrite.v384logplain
-rw-r--r--Sum.out99logplain
-rw-r--r--Sum.v93logplain
-rw-r--r--Tactics.out130logplain
-rw-r--r--Tactics.v357logplain
-rw-r--r--TranspModtype.out89logplain
-rw-r--r--TranspModtype.v385logplain
-rw-r--r--ZSyntax.out578logplain
-rw-r--r--ZSyntax.v558logplain
-rw-r--r--inference.out563logplain
-rw-r--r--inference.v881logplain
-rw-r--r--ltac.out1370logplain
-rw-r--r--ltac.v1261logplain
-rw-r--r--names.out168logplain
-rw-r--r--names.v132logplain
-rw-r--r--onlyprinting.out18logplain
-rw-r--r--onlyprinting.v107logplain
-rw-r--r--qualification.out172logplain
-rw-r--r--qualification.v324logplain
-rw-r--r--reduction.out44logplain
-rw-r--r--reduction.v279logplain
-rw-r--r--rewrite-2172.out91logplain
-rw-r--r--rewrite-2172.v734logplain
-rw-r--r--set.out276logplain
-rw-r--r--set.v154logplain
-rw-r--r--simpl.out198logplain
-rw-r--r--simpl.v148logplain
-rw-r--r--subst.out1242logplain
-rw-r--r--subst.v1588logplain
-rw-r--r--unifconstraints.out1487logplain
-rw-r--r--unifconstraints.v655logplain