aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
2020-04-01add tests for notations with sigma typesOlivier Laurent
2020-03-31Remove special case for implicit inductive parametersMaxime Dénès
2020-03-31Merge PR #11668: Helping issue #11659 by leaving only the Cast hack in the gr...Maxime Dénès
2020-03-29Merge PR #11859: Warn when non exactly parsing non floating-pointHugo Herbelin
2020-03-27Helping issue #11659 by leaving only the Cast hack in the grammar.Hugo Herbelin
2020-03-26Print a warning when parsing non floating-point values.Pierre Roux
2020-03-25Nicer printing for decimal constants in QPierre Roux
2020-03-25Nicer printing for decimal constants in RPierre Roux
2020-03-22Testing notations which are specific numerals.Hugo Herbelin
2020-03-22Adding a test for printing single characters.Hugo Herbelin
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-19Merge PR #11760: firstorder: default tactic is “auto with core”Théo Zimmermann
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
2020-03-19Merge PR #11822: Grants #11692: clear dependent knows about let-inPierre-Marie Pédrot
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-18Change some ouput tests due to the printing of implicitsSimonBoulier
2020-03-14Fixes #11692 (clear dependent knows about let-in).Hugo Herbelin
2020-03-10Fixing little bug in parsing decimal numbers in R.Hugo Herbelin
2020-03-05Merge PR #11602: Adding support for an "only parsing" modifier in "where"-bas...Pierre-Marie Pédrot
2020-03-04Adding support for an "only parsing" modifier in "where"-based notations.Hugo Herbelin
2020-02-29Be robust in calculating visible ids for non-registered constants.Pierre-Marie Pédrot
2020-02-28Merge PR #11609: [stm] Use Default Proof Using only with ProofEnrico Tassi
2020-02-28[stm] Use Default Proof Using only with ProofTej Chajed
2020-02-27Merge PR #11650: Set Printing ParensEmilio Jesus Gallego Arias
2020-02-25Use implicit arguments in notations for eq.Gaëtan Gilbert
2020-02-23Adding tests for Set Printing Parentheses.Hugo Herbelin
2020-02-22New parsing/printing pattern/terms imp/scopes tests summarizing last changes.Hugo Herbelin
2020-02-22In printing patterns, distinguish the case of a notation to @id.Hugo Herbelin
2020-02-22Use auxiliary function for externing record patterns.Hugo Herbelin
2020-02-22Propagate implicit arguments in all notations for partial applications.Hugo Herbelin
2020-02-22Deactivate implicit arguments in printing notations bound to "@f".Hugo Herbelin
2020-02-22Fixing printing of notations bound to an expression of the form "@f".Hugo Herbelin
2020-02-22Fixing a notation printing bug (missing a @ to reflect absence of imp. args).Hugo Herbelin
2020-02-22Fixing anomaly from #11091 (incompatible printing with notation and imp. args).Hugo Herbelin
2020-02-22Merge PR #11596: ComInductive: use lbound=Prop iff non polymorphicEmilio Jesus Gallego Arias
2020-02-21Merge PR #11261: Use implicit types for printing (granting wish #10366).Emilio Jesus Gallego Arias
2020-02-21Merge PR #11142: Slightly improving strategy about when to print coercion or ...Emilio Jesus Gallego Arias
2020-02-20[test-suite] Fix output tests due to merge problems.Emilio Jesus Gallego Arias
2020-02-20Merge PR #11143: In Print/Check/Show, adopt the view that the attached type i...Emilio Jesus Gallego Arias
2020-02-20Merge PR #10832: Addressing #6082 and #7766: warning when overriding notation...Emilio Jesus Gallego Arias
2020-02-19Revert "Granting #9516 and #9518 (support for numerals and strings in custom ...Hugo Herbelin
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
2020-02-19ComInductive: use lbound=Prop iff non polymorphicGaëtan Gilbert
2020-02-17Take "Implicit Types" into account when printing terms.Hugo Herbelin
2020-02-17Mini-improvements in when to skip coercions or explicitly print implicit args.Hugo Herbelin
2020-02-16Revert "Suite picking numeral notation"Hugo Herbelin
2020-02-16Suite picking numeral notationHugo Herbelin
2020-02-16Granting #9516 and #9518 (support for numerals and strings in custom entries).Hugo Herbelin
2020-02-15Fixes #11331 (unexpected level collisions between custom entries and constr).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:57:38 +0000