aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-09Merge PR #12163: Fix #12159 (Numeral Notations do not play well with multiple...Hugo Herbelin
2020-05-09Merge PR #12263: HaskellExtr: Add type annotations to Prelude.==Kazuhiko Sakaguchi
2020-05-06HaskellExtr: Add type annotations to Prelude.==Jason Gross
2020-05-02Fix #12159 (Numeral Notations do not play well with multiple scopes for the s...Pierre Roux
2020-05-01Testing different combinations of non truly recursive (co)fixpoints.Hugo Herbelin
2020-04-28Merge PR #12003: Improve error messages for Set and Unset commands.Emilio Jesus Gallego Arias
2020-04-22Merge PR #11694: Support printing argument-free abbreviations in custom entri...Emilio Jesus Gallego Arias
2020-04-20Improve undeclared key messages.Théo Zimmermann
2020-04-17Merge PR #11135: Simplifying the code declaring the constants bound to primit...Pierre-Marie Pédrot
2020-04-16Merge PR #12101: Add needed commas in messageGaëtan Gilbert
2020-04-15Add needed commas in messageJim Fehrle
2020-04-15[proof] Move functions related to `Proof.t` to `Proof`Emilio Jesus Gallego Arias
2020-04-14Merge PR #11957: [stdlib] update sigma-type notationsHugo Herbelin
2020-04-14Merge PR #11820: Partial importsMaxime Dénès
2020-04-13Add specific test for "useless" syndefGaëtan Gilbert
2020-04-13Simplifying the declaration of constants bound to primitive projections.Hugo Herbelin
2020-04-11If a custom entry has global, a bound variable is valid in this entry.Hugo Herbelin
2020-04-11If a custom entry has global, an argument-free abbreviation is valid in this ...Hugo Herbelin
2020-04-06Fix #11934 equality on constrexpr ignores instances of explicit applicationsGaëtan Gilbert
2020-04-03Improve error messages for Set and Unset commands.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-31 05:52:13 +0000