aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
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
2019-12-23Fixes a small bug exposing an _ANONYMOUS_REL in a unification error message.Hugo Herbelin
2019-12-20Coherence checking for coercionsKazuhiko Sakaguchi
2019-12-18Merge PR #11203: Make the string argument of `time` print correctlyPierre-Marie Pédrot
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
2019-12-08When printing term together with its type, use info that term is in context.Hugo Herbelin
2019-12-06Make the string argument of `time` print correctlyJason Gross
2019-12-03Printing: Interleaving search for notations and removal of coercions.Hugo Herbelin
2019-12-03Fixes #11231 (missing dependency in pattern-matching decompilation).Hugo Herbelin
2019-11-29Merge PR #11076: Remove all remaining calls to “omega” from the standard ...Emilio Jesus Gallego Arias
2019-11-26Merge PR #11090: Printing of coercions to which a notation is associated: a r...Emilio Jesus Gallego Arias
2019-11-25Test-suite: avoid using “omega”Vincent Laporte
2019-11-21A refined version of #8890 which prevents #11033.Hugo Herbelin
2019-11-20Combine similar arguments when printing Arguments commandGaëtan Gilbert
2019-11-11Miscellaneous improvements of the syntax of records.Hugo Herbelin
2019-11-01Add extraction for primitive floatsErik Martin-Dorel
2019-11-01Make primitive float work on WindowsPierre Roux
2019-11-01Pretty-printing primitive float constantsErik Martin-Dorel
2019-10-31Merge PR #10985: Print argument info as an Arguments command in AboutEmilio Jesus Gallego Arias
2019-10-31Merge PR #9883: Add support for Sorts in numeral notationsVincent Laporte
2019-10-31restore red behaviour printingGaëtan Gilbert
2019-10-31Fix output testsGaëtan Gilbert
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
2019-10-28Add support for Sorts in numeral notationsJason Gross
2019-10-17Fix Locate printing regressionGuillaume Melquiond
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
2019-10-05Fix #10669 incorrect substitution in context outside sectionGaëtan Gilbert
2019-10-04Allow SProp default onGaëtan Gilbert
2019-09-16Re-implementation of zifyFrédéric Besson
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 05:28:29 +0000