aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
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-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
2019-09-09[stdlib] Do not put INR_eq in the “real” hint databaseVincent Laporte
2019-09-04Merge PR #10577: Fix #7348: extraction of dependent record projectionsMaxime Dénès
2019-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
2019-09-02Merge PR #10648: [extraction] Fix #7191: Avoid unsound eta-reductionMaxime Dénès
2019-08-29Make sure that all query commands return a notice (not an info) feedbackMaxime Dénès
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-10[extraction] Fix #7191: Avoid unsound eta-reductionKazuhiko Sakaguchi
2019-08-08Fix regression of #10637 (-emacs arg sets color to `EMACS)Jim Fehrle
2019-07-31Fix #7348: extraction of dependent record projectionsKazuhiko Sakaguchi
2019-07-02Improve the ambiguous paths warning to indicate which path is ambiguous with ...Kazuhiko Sakaguchi