aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2020-04-28Merge PR #12003: Improve error messages for Set and Unset commands.Emilio Jesus Gallego Arias
2020-04-27Merge PR #12073: Split off Nsatz tactic part into Nsatz_tacticPierre-Marie Pédrot
2020-04-27Merge PR #12175: Calculation speed of Cauchy realsMichael Soegtrop
2020-04-26constructive square rootVincent Semeria
2020-04-24Make the nsatz test-suite passJason Gross
2020-04-24Add memory stats to tables by defaultJason Gross
2020-04-24Split off Nsatz tactic part into NsatzTacticJason Gross
2020-04-22Merge PR #12023: Adding a Declare ML Module in empty file Ltac.vEmilio Jesus Gallego Arias
2020-04-22Merge PR #11694: Support printing argument-free abbreviations in custom entri...Emilio Jesus Gallego Arias
2020-04-21Adapt test-suite to #12023.Hugo Herbelin
2020-04-21Fixing #3451: coqdoc links for projections of tuples rather than for construc...Hugo Herbelin
2020-04-21Merge PR #12082: Fixes #11808: support for test-suite in -byte-only modeGaëtan Gilbert
2020-04-21Merge PR #12116: Fixing #12045: missing normalization in conclusion of custom...Pierre-Marie Pédrot
2020-04-21Merge PR #11883: Fix #7812: autounfold's behavior depends on file namesHugo Herbelin
2020-04-20Merge PR #12038: Improve undeclared goption key messages.Gaëtan Gilbert
2020-04-20Merge PR #12126: TIMEFMT: Display the output file nameGaëtan Gilbert
2020-04-20Granting coqdoc wish #7093 (definitions link to themselves).Hugo Herbelin
2020-04-20TIMEFMT: Display the output file nameJason Gross
2020-04-20Improve undeclared key messages.Théo Zimmermann
2020-04-20Fixing #12045 (missing normalization in conclusion of custom induction scheme).Hugo Herbelin
2020-04-19Fix Makefile warning: undefined variable '*'Jason Gross
2020-04-19Merge PR #12033: Let coqdoc be informed by coq about binding variables (incid...Lysxia
2020-04-17ZArith: move lia hints to a dedicated moduleVincent Laporte
2020-04-17Merge PR #11135: Simplifying the code declaring the constants bound to primit...Pierre-Marie Pédrot
2020-04-17Merge PR #11972: Fix require in sectionPierre-Marie Pédrot
2020-04-16Merge PR #12070: Ignore -native-compiler option when disabledPierre-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-15Coqdoc: Exporting location and unique id for binding variables.Hugo Herbelin
2020-04-15[proof] Move functions related to `Proof.t` to `Proof`Emilio Jesus Gallego Arias
2020-04-15Ignore -native-compiler option when disabledPierre Roux
2020-04-14Merge PR #11957: [stdlib] update sigma-type notationsHugo Herbelin
2020-04-14Merge PR #11820: Partial importsMaxime Dénès
2020-04-14Merge PR #11978: Close #11935: section variables do not have universe instances.Pierre-Marie Pédrot
2020-04-14Merge PR #11985: Fix #11934 equality on constrexpr ignores instances of expli...Pierre-Marie Pédrot
2020-04-13Close #11935: section variables do not have universe instances.Gaëtan Gilbert
2020-04-13Fix #11783 Require in SectionGaëtan Gilbert
2020-04-13Partial import inductive(..)Gaëtan Gilbert
2020-04-13test partial importGaëtan Gilbert
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-12Exporting BEST as OPT for the tests using coq_makefile-generated Makefile.Hugo Herbelin
2020-04-12[test-suite] Remove deprecated -I option of coqchk in MakefilePierre Roux
2020-04-11Fix #7812Attila Gáspár
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-10[obligations] Deprecated flag cleanupEmilio Jesus Gallego Arias
2020-04-07Support universe bindings and universe constraints in Let definitions.Théo Zimmermann
2020-04-06Fix #11934 equality on constrexpr ignores instances of explicit applicationsGaëtan Gilbert
2020-04-06Merge PR #11955: Use the kernel machine in whd_betaiota_deltazeta_for_iota_stateMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 06:09:00 +0000