aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
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
2020-02-13Merge PR #11098: Let Arguments support anonymous implicit argumentsEmilio Jesus Gallego Arias
2020-02-13Merge PR #11424: Check instance length in type_of_{inductive,constructor}Pierre-Marie Pédrot
2020-02-13Arguments: removing the restriction to set an anonymous parameter implicit.Hugo Herbelin
2020-02-12Merge PR #11563: Mini improvement of the formatting rule for printing fix and...Gaëtan Gilbert
2020-02-12Check instance length in type_of_{inductive,constructor}Gaëtan Gilbert
2020-02-12Merge PR #11573: Fixing extra space in front of keywords in Print GrammarEmilio Jesus Gallego Arias
2020-02-11Fixing extra space in "Print Grammar" (i.e. Grammar.Entry.print in Gramlib).Hugo Herbelin
2020-02-11Fixing some residual bugs of PR #10202 (manual implicit args in subterms).Hugo Herbelin
2020-02-11Small improvement to "fix"/"cofix" printing rule.Hugo Herbelin
2020-02-08Merge PR #11240: Add rew dependent NotationsHugo Herbelin
2020-02-06Merge PR #10835: Accepting a few more variants of format for recursive notati...Pierre-Marie Pédrot
2020-01-31More tolerant in format for recursive notations.Hugo Herbelin
2020-01-30Printing tests for applied references combined with impl. args. and notations.Hugo Herbelin
2020-01-28Fix #11467Pierre Roux
2020-01-14Merge PR #10486: [extraction] Support extraction of Coq's string type to OCam...Kazuhiko Sakaguchi
2020-01-13Merge PR #11280: Fix #11195 and add other improvements: try loading .vio (and...Pierre-Marie Pédrot
2020-01-08Add test case for string extraction in OCaml and HaskellMaxime Dénès
2020-01-08replace deprecated -quick with -vio in the test suiteEnrico Tassi
2019-12-30Merge PR #11233: Fixes #11231: missing dependency in looking for default clau...Pierre-Marie Pédrot
2019-12-29Merge PR #11334: Fixes a small bug exposing an _ANONYMOUS_REL in a unificatio...Pierre-Marie Pédrot
2019-12-28Extend `Print Canonical Projections` with a search functionalityKazuhiko Sakaguchi
2019-12-26Add rew dependent NotationsJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 13:03:12 +0000