aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2020-04-28Merge PR #12003: Improve error messages for Set and Unset commands.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: jfehrle
2020-04-27Merge PR #12073: Split off Nsatz tactic part into Nsatz_tacticPierre-Marie Pédrot
Reviewed-by: anton-trunov Reviewed-by: ppedrot
2020-04-27Merge PR #12175: Calculation speed of Cauchy realsMichael Soegtrop
Reviewed-by: MSoegtropIMC
2020-04-26constructive square rootVincent Semeria
Convert into a performance test Put time bound at the beginning of file Add Time command in the test
2020-04-24Make the nsatz test-suite passJason Gross
2020-04-24Add memory stats to tables by defaultJason Gross
The Python scripts now support `--no-include-mem` to turn it off, and also support `--sort-by-mem`. Closes #11575
2020-04-24Split off Nsatz tactic part into NsatzTacticJason Gross
Closes #5445 Note that we use `Include` rather than `Export` to expose the machinery defined in `NsatzTactic` from `Nsatz` to preserve backwards compatibility with developments relying on absolute names of the constants previously defined in `Nsatz.v`.
2020-04-22Merge PR #12023: Adding a Declare ML Module in empty file Ltac.vEmilio Jesus Gallego Arias
Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: ppedrot
2020-04-22Merge PR #11694: Support printing argument-free abbreviations in custom ↵Emilio Jesus Gallego Arias
entries with a global rule Reviewed-by: ejgallego Ack-by: gares
2020-04-21Adapt test-suite to #12023.Hugo Herbelin
2020-04-21Fixing #3451: coqdoc links for projections of tuples rather than for ↵Hugo Herbelin
constructor. Moreover, the link to the constructor was hiding other contents of the tuple.
2020-04-21Merge PR #12082: Fixes #11808: support for test-suite in -byte-only modeGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-21Merge PR #12116: Fixing #12045: missing normalization in conclusion of ↵Pierre-Marie Pédrot
custom induction scheme Reviewed-by: ppedrot
2020-04-21Merge PR #11883: Fix #7812: autounfold's behavior depends on file namesHugo Herbelin
Reviewed-by: herbelin
2020-04-20Merge PR #12038: Improve undeclared goption key messages.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-20Merge PR #12126: TIMEFMT: Display the output file nameGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-20Granting coqdoc wish #7093 (definitions link to themselves).Hugo Herbelin
Co-Authored-By: Xia Li-yao <Lysxia@users.noreply.github.com>
2020-04-20TIMEFMT: Display the output file nameJason Gross
We now use `$@` rather than `$*` so that we display the output target rather than the stem of the rule. This is more consistent for rules that users add (where the pattern variable might be something insufficiently identifying), and also generalizes more nicely to mixing multiple compilers (we get a clear difference between producing OCaml files and producing .vo files, even if the filename is the same up to the suffix). The result is that it's easy to describe what the timing information of the build log records: each time comes with a label which is a file name, and the time is the time it takes to produce that file.
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
We fix ``` Makefile.build:222: warning: undefined variable '*' ``` by not passing a time format including a Makefile variable when not inside a target (and whether or not the command succeeds should not depend on the particular format in any case, and all we are testing for is whether or not the command exists and supports `-f`).
2020-04-19Merge PR #12033: Let coqdoc be informed by coq about binding variables ↵Lysxia
(incidentally fixes #7697) Reviewed-by: 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 ↵Pierre-Marie Pédrot
primitive projections Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot
2020-04-17Merge PR #11972: Fix require in sectionPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-04-16Merge PR #12070: Ignore -native-compiler option when disabledPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-04-16Merge PR #12101: Add needed commas in messageGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-15Add needed commas in messageJim Fehrle
2020-04-15Coqdoc: Exporting location and unique id for binding variables.Hugo Herbelin
This provides linking, appropriate coloring and appropriate hovering in coqdoc documents. In particular, this fixes #7697.
2020-04-15[proof] Move functions related to `Proof.t` to `Proof`Emilio Jesus Gallego Arias
This makes the API more orthogonal and allows better structure in future code.
2020-04-15Ignore -native-compiler option when disabledPierre Roux
2020-04-14Merge PR #11957: [stdlib] update sigma-type notationsHugo Herbelin
Reviewed-by: JasonGross Ack-by: herbelin
2020-04-14Merge PR #11820: Partial importsMaxime Dénès
Reviewed-by: Zimmi48 Reviewed-by: jfehrle Reviewed-by: maximedenes Ack-by: ppedrot
2020-04-14Merge PR #11978: Close #11935: section variables do not have universe instances.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-14Merge PR #11985: Fix #11934 equality on constrexpr ignores instances of ↵Pierre-Marie Pédrot
explicit applications Ack-by: herbelin Reviewed-by: ppedrot
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
NB: 3 dots doesn't play well with PG's sentence detection.
2020-04-13test partial importGaëtan Gilbert
2020-04-13Add specific test for "useless" syndefGaëtan Gilbert
This happens in practice with the list syndef in List.v
2020-04-13Simplifying the declaration of constants bound to primitive projections.Hugo Herbelin
We factorize code from declareInd.ml and inductiveops.ml which was already existing in record.ml. We keep expansion of local definitions in the type of fields of primitive records while these are not expanded in the non-primitive case. This is to be consistent with what Indtypes.compute_projections is doing. See discussion at #11135. We keep the unused code from inductiveops.ml for possible future use though. Include improvements contributed by Gaëtan Gilbert.
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
This is due to "global" being a syntactic notation, thus including ident. Parsing was automatically supporting this. This commit adds support for printing.
2020-04-11If a custom entry has global, an argument-free abbreviation is valid in this ↵Hugo Herbelin
entry. Parsing was automatically supporting this. This commit adds support for printing. Note: It would be more delicate to recognize that some given entry support applicative nodes hence abbreviations with arguments.
2020-04-10[obligations] Deprecated flag cleanupEmilio Jesus Gallego Arias
We deprecate `Hide Obligations` and remove `Shrink Obligations` [deprecated since 8.7]
2020-04-07Support universe bindings and universe constraints in Let definitions.Théo Zimmermann
Let vs Definition / Example syntax was split in 7c28130 for parsing reasons: so that the new Let Fixpoint and Let CoFixpoint syntax could be introduced. This split is probably the reason why Let was overlooked when support for universe bindings and universe constraints were added to Definition and variants.
2020-04-06Fix #11934 equality on constrexpr ignores instances of explicit applicationsGaëtan Gilbert
While we're at it also compare instances in glob_constr although I don't know if that changes any behaviour.
2020-04-06Merge PR #11955: Use the kernel machine in whd_betaiota_deltazeta_for_iota_stateMatthieu Sozeau
Reviewed-by: SkySkimmer Reviewed-by: mattam82
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 12:36:22 +0000