/test-suite/output/

• ../
• Arguments.out
• Arguments.v
• ArgumentsScope.out
• ArgumentsScope.v
• Arguments_renaming.out
• Arguments_renaming.v
• Binder.out
• Binder.v
• Cases.out
• Cases.v
• Coercions.out
• Coercions.v
• CompactContexts.out
• CompactContexts.v
• ErrorInModule.out
• ErrorInModule.v
• ErrorInSection.out
• ErrorInSection.v
• Errors.out
• Errors.v
• Existentials.out
• Existentials.v
• Extraction_matchs_2413.out
• Extraction_matchs_2413.v
• Fixpoint.out
• Fixpoint.v
• FunExt.out
• FunExt.v
• Implicit.out
• Implicit.v
• Inductive.out
• Inductive.v
• InitSyntax.out
• InitSyntax.v
• Int31Syntax.out
• Int31Syntax.v
• Intuition.out
• Intuition.v
• Match_subterm.out
• Match_subterm.v
• Nametab.out
• Nametab.v
• Naming.out
• Naming.v
• Notations.out
• Notations.v
• Notations2.out
• Notations2.v
• Notations3.out
• Notations3.v
• PatternsInBinders.out
• PatternsInBinders.v
• PrintAssumptions.out
• PrintAssumptions.v
• PrintInfos.out
• PrintInfos.v
• PrintModule.out
• PrintModule.v
• Quote.out
• Quote.v
• RealSyntax.out
• RealSyntax.v
• RecognizePluginWarning.out
• RecognizePluginWarning.v
• Record.out
• Record.v
• Search.out
• Search.v
• SearchHead.out
• SearchHead.v
• SearchPattern.out
• SearchPattern.v
• SearchRewrite.out
• SearchRewrite.v
• Show.out
• Show.v
• ShowMatch.out
• ShowMatch.v
• ShowProof.out
• ShowProof.v
• Sum.out
• Sum.v
• Tactics.out
• Tactics.v
• TranspModtype.out
• TranspModtype.v
• TypeclassDebug.out
• TypeclassDebug.v
• UnclosedBlocks.out
• UnclosedBlocks.v
• UnivBinders.out
• UnivBinders.v
• UsePluginWarning.out
• UsePluginWarning.v
• Warnings.out
• Warnings.v
• ZSyntax.out
• ZSyntax.v
• auto.out
• auto.v
• goal_output.out
• goal_output.v
• inference.out
• inference.v
• ltac.out
• ltac.v
• ltac_missing_args.out
• ltac_missing_args.v
• names.out
• names.v
• onlyprinting.out
• onlyprinting.v
• qualification.out
• qualification.v
• reduction.out
• reduction.v
• rewrite-2172.out
• rewrite-2172.v
• set.out
• set.v
• simpl.out
• simpl.v
• subst.out
• subst.v
• unifconstraints.out
• unifconstraints.v