aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
ModeNameSize
-rw-r--r--Arguments.out3449logplain
-rw-r--r--Arguments.v1470logplain
-rw-r--r--ArgumentsScope.out1083logplain
-rw-r--r--ArgumentsScope.v560logplain
-rw-r--r--Arguments_renaming.out4329logplain
-rw-r--r--Arguments_renaming.v1049logplain
-rw-r--r--Binder.out168logplain
-rw-r--r--Binder.v134logplain
-rw-r--r--Cases.out4548logplain
-rw-r--r--Cases.v6316logplain
-rw-r--r--Coercions.out108logplain
-rw-r--r--Coercions.v651logplain
-rw-r--r--CompactContexts.out142logplain
-rw-r--r--CompactContexts.v141logplain
-rw-r--r--ErrorInModule.out116logplain
-rw-r--r--ErrorInModule.v101logplain
-rw-r--r--ErrorInSection.out116logplain
-rw-r--r--ErrorInSection.v102logplain
-rw-r--r--Errors.out451logplain
-rw-r--r--Errors.v548logplain
-rw-r--r--Existentials.out237logplain
-rw-r--r--Existentials.v225logplain
-rw-r--r--Extraction_infix.out279logplain
-rw-r--r--Extraction_infix.v623logplain
-rw-r--r--Extraction_matchs_2413.out1058logplain
-rw-r--r--Extraction_matchs_2413.v2778logplain
-rw-r--r--Fixpoint.out519logplain
-rw-r--r--Fixpoint.v1177logplain
-rw-r--r--FunExt.out866logplain
-rw-r--r--FunExt.v4767logplain
-rw-r--r--Implicit.out391logplain
-rw-r--r--Implicit.v1265logplain
-rw-r--r--Inductive.out143logplain
-rw-r--r--Inductive.v94logplain
-rw-r--r--InitSyntax.out433logplain
-rw-r--r--InitSyntax.v111logplain
-rw-r--r--Int31Syntax.out154logplain
-rw-r--r--Int31Syntax.v431logplain
-rw-r--r--Intuition.out85logplain
-rw-r--r--Intuition.v121logplain
-rw-r--r--InvalidDisjunctiveIntro.out769logplain
-rw-r--r--InvalidDisjunctiveIntro.v888logplain
-rw-r--r--MExtraction.v377logplain
-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.out3619logplain
-rw-r--r--Notations.v8889logplain
-rw-r--r--Notations2.out2017logplain
-rw-r--r--Notations2.v4899logplain
-rw-r--r--Notations3.out4438logplain
-rw-r--r--Notations3.v8884logplain
-rw-r--r--PatternsInBinders.out1239logplain
-rw-r--r--PatternsInBinders.v1704logplain
-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--RecognizePluginWarning.out0logplain
-rw-r--r--RecognizePluginWarning.v289logplain
-rw-r--r--Record.out628logplain
-rw-r--r--Record.v822logplain
-rw-r--r--Search.out4430logplain
-rw-r--r--Search.v1253logplain
-rw-r--r--SearchHead.out1411logplain
-rw-r--r--SearchHead.v460logplain
-rw-r--r--SearchPattern.out2215logplain
-rw-r--r--SearchPattern.v1003logplain
-rw-r--r--SearchRewrite.out120logplain
-rw-r--r--SearchRewrite.v384logplain
-rw-r--r--Show.out148logplain
-rw-r--r--Show.v267logplain
-rw-r--r--ShowMatch.out58logplain
-rw-r--r--ShowMatch.v349logplain
-rw-r--r--ShowProof.out31logplain
-rw-r--r--ShowProof.v145logplain
-rw-r--r--SuggestProofUsing.out222logplain
-rw-r--r--SuggestProofUsing.v547logplain
-rw-r--r--Sum.out99logplain
-rw-r--r--Sum.v93logplain
-rw-r--r--Tactics.out256logplain
-rw-r--r--Tactics.v562logplain
-rw-r--r--TranspModtype.out89logplain
-rw-r--r--TranspModtype.v385logplain
-rw-r--r--TypeclassDebug.out864logplain
-rw-r--r--TypeclassDebug.v227logplain
-rw-r--r--UnclosedBlocks.out76logplain
-rw-r--r--UnclosedBlocks.v250logplain
-rw-r--r--UnivBinders.out4840logplain
-rw-r--r--UnivBinders.v4167logplain
-rw-r--r--UsePluginWarning.out14logplain
-rw-r--r--UsePluginWarning.v141logplain
-rw-r--r--Warnings.out187logplain
-rw-r--r--Warnings.v177logplain
-rw-r--r--ZSyntax.out578logplain
-rw-r--r--ZSyntax.v558logplain
-rw-r--r--auto.out544logplain
-rw-r--r--auto.v169logplain
-rw-r--r--bug5778.out189logplain
-rw-r--r--bug5778.v124logplain
-rw-r--r--goal_output.out98logplain
-rw-r--r--goal_output.v205logplain
-rw-r--r--idtac.out85logplain
-rw-r--r--idtac.v997logplain
-rw-r--r--inference.out559logplain
-rw-r--r--inference.v923logplain
-rw-r--r--ltac.out1472logplain
-rw-r--r--ltac.v1469logplain
-rw-r--r--ltac_extra_args.out378logplain
-rw-r--r--ltac_extra_args.v135logplain
-rw-r--r--ltac_missing_args.out1813logplain
-rw-r--r--ltac_missing_args.v384logplain
-rw-r--r--names.out275logplain
-rw-r--r--names.v228logplain
-rw-r--r--onlyprinting.out18logplain
-rw-r--r--onlyprinting.v107logplain
-rw-r--r--optimize_heap.out102logplain
-rw-r--r--optimize_heap.v108logplain
-rw-r--r--qualification.out173logplain
-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