| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-03 | Merge PR #8877: Fix #8876: expected number of arguments for cumulative ↵ | Pierre-Marie Pédrot | |
| constructors | |||
| 2018-11-03 | Merge PR #8745: Fixes #3468: making tactic-in-term sensitive to ↵ | Pierre-Marie Pédrot | |
| interpretation scopes | |||
| 2018-11-02 | Remove is_universe_polymorphism from printing | Gaëtan Gilbert | |
| 2018-11-02 | Remove incorrect is_universe_polymorphism from modintern | Gaëtan Gilbert | |
| 2018-11-02 | Make attributes more general to make defining #[universes(...)] easy | Gaëtan Gilbert | |
| 2018-11-02 | gitignore test-suite/misc/poly-capture-global-univs/src/evil.ml | Gaëtan Gilbert | |
| With camlp4 this file was not created but now that we use mlg it has appeared. | |||
| 2018-11-02 | Fixing one instance of bug #8224 (grounding term w/o knowing if it has evars). | Hugo Herbelin | |
| 2018-10-31 | Partial fix of #8706 (tactic-in-term sensitive to seemingly unrelated scopes). | Hugo Herbelin | |
| We compute the binding to tactic-in-term once for all in the right scopes before interpreting the tactic. An alternative would have been to surround the constr_expr by CDelimiters to simulate its interpretation in the expected scopes (though this would not have worked for temporary scopes). | |||
| 2018-10-31 | [ssr] better doc for the IPatDispatch AST | Enrico Tassi | |
| 2018-10-31 | test-suite entry for issue #8544 | Cyril Cohen | |
| 2018-10-31 | Merge PR #8759: Fix #8755: Uncaught exception ↵ | Hugo Herbelin | |
| Ltac_plugin.Taccoerce.CannotCoerceTo. | |||
| 2018-10-31 | Fix #8881: validate fails to use inductive equivalence in case_info | Gaëtan Gilbert | |
| See also 55dbe8e2fa7ed2053ecd54140f6bcbdf31981e0b | |||
| 2018-10-31 | Fix #8876: expected number of arguments for cumulative constructors | Gaëtan Gilbert | |
| ee573583701c8e53e8b82978998a9df93170cd79 ported to the checker. | |||
| 2018-10-31 | Fix #8873: coqchk on inductive with letin parameter | Gaëtan Gilbert | |
| 2018-10-31 | No need to require List in test-suite/success/Inductive.v | Gaëtan Gilbert | |
| Requires are slow in the debugger so removing this makes it nicer to debug. | |||
| 2018-10-31 | Notations: fixing a bug with abbreviations in custom entries. | Hugo Herbelin | |
| Coercions were missing. | |||
| 2018-10-29 | Fix for bug #8848 | Matthieu Sozeau | |
| 2018-10-29 | Merge PR #8737: Correctly report non-projection fields in records | Pierre-Marie Pédrot | |
| 2018-10-29 | Merge PR #8763: Adapt coq_makefile to handle coqpp-based macro files. | Enrico Tassi | |
| 2018-10-26 | Add record names to multiple records error message | Tej Chajed | |
| 2018-10-26 | Correctly report non-projection fields in records | Tej Chajed | |
| Fixes #8736. | |||
| 2018-10-23 | Fixing #8794 (anomaly with abbreviation involving both term and binders). | Hugo Herbelin | |
| 2018-10-21 | Adding a regression test for bug #8785 (missing univ constraints registration). | Hugo Herbelin | |
| 2018-10-19 | Porting the test-suite to coqpp. | Pierre-Marie Pédrot | |
| 2018-10-19 | Fix #8755: Uncaught exception Ltac_plugin.Taccoerce.CannotCoerceTo. | Pierre-Marie Pédrot | |
| 2018-10-16 | Merge PR #8059: Simplify code for [Definition := Eval ...] | Matthieu Sozeau | |
| 2018-10-16 | [test-suite] Update csdp cache | Vincent Laporte | |
| 2018-10-15 | Correct some spelling errors | Benjamin Barenblat | |
| Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`. | |||
| 2018-10-11 | Merge PR #8594: Miscellaneous refinements and cleaning of module printing | Emilio Jesus Gallego Arias | |
| 2018-10-11 | [dune] [test-suite] Support for running the test suite with Dune. | Emilio Jesus Gallego Arias | |
| 2018-10-11 | Merge PR #186: [RFC] Coqlib cleanup | Pierre-Marie Pédrot | |
| 2018-10-11 | [test-suite] Use the right OCAMLPATH separator on Windows. | Emilio Jesus Gallego Arias | |
| Hopefully this goes away when OCAMLPATH is properly handled by the build system. | |||
| 2018-10-10 | Miscellaneous refinements/cleaning of module printing. | Hugo Herbelin | |
| This refines the fix to #2169 by distinguishing the short and non-short printing modes. This prepares functionalization of printers by always passing env rather than setting env to None in short mode. This is not strictly necessary for the env which is not used for printing global references but it shall be more consistent in style when passing e.g. the nametab functionally. We however keep the fallback printer used in case of error while printing: due to missing registration of submodule fields in the nametab, printing with types does not work if there are references to an inner module. | |||
| 2018-10-10 | [coqlib] Rebindable Coqlib namespace. | Emilio Jesus Gallego Arias | |
| We refactor the `Coqlib` API to locate objects over a namespace `module.object.property`. This introduces the vernacular command `Register g as n` to expose the Coq constant `g` under the name `n` (through the `register_ref` function). The constant can then be dynamically located using the `lib_ref` function. Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org> Co-authored-by: Maxime Dénès <mail@maximedenes.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr> | |||
| 2018-10-10 | [test-suite] Don't reset `OCAMLPATH`, but append to it. | Emilio Jesus Gallego Arias | |
| This fixes an obvious bug introduced in #8602. | |||
| 2018-10-10 | [test-suite] rename a file | Vincent Laporte | |
| 2018-10-10 | Merge PR #6218: Fix #5197, handling of algebraic universes | Pierre-Marie Pédrot | |
| 2018-10-10 | Merge PR #8602: [test-suite] Use ocamlfind to locate Coq libraries in unit ↵ | Enrico Tassi | |
| tests. | |||
| 2018-10-10 | Merge PR #8679: [test suite] Compile test cases, instead of only loading them | Enrico Tassi | |
| 2018-10-09 | [default.nix] Add install dir to OCAMLPATH before running the test-suite | Vincent Laporte | |
| 2018-10-09 | [test-suite] use “-async-proofs-cache force” when compiling | Vincent Laporte | |
| 2018-10-09 | [test-suite] Use ocamlfind to locate Coq libraries in unit tests. | Emilio Jesus Gallego Arias | |
| This is slightly more robust and allows to run the test suite with Dune which may place OCaml objects differently. | |||
| 2018-10-09 | [test-suite] compile (rather than load) test cases | Vincent Laporte | |
| 2018-10-09 | [test-suite] ensure file names are valid module names | Vincent Laporte | |
| 2018-10-09 | Simplify code for [Definition := Eval ...] | Gaëtan Gilbert | |
| Note that since this now reduces before restricting universes behaviour may be a bit different. | |||
| 2018-10-09 | Fix nativenorm when an evar is in the wrong place. | Gaëtan Gilbert | |
| See commit [Simplify code for [Definition := Eval ...]] which without this breaks test suite 7631.v | |||
| 2018-10-09 | Refactoring of Micromega code using a Simplex linear solver | Frédéric Besson | |
| - Simplex based linear prover Unset Simplex to get Fourier elimination For lia and nia, do not enumerate but generate cutting planes. - Better non-linear support Factorisation of the non-linear pre-processing Careful handling of equation x=e, x is only eliminated if x is used linearly - More opaque interfaces (Linear solvers Simplex and Mfourier are independent) - Set Dump Arith "file" so that lia,nia calls generate Coq goals in filexxx.v. Used to collect benchmarks and regressions. - Rationalise the test-suite example.v only tests psatz Z example_nia.v only tests lia, nia In both files, the tests are in essence the same. In particular, if a test is solved by psatz but not by nia, we finish the goal by an explicit Abort. There are additional tests in example_nia.v which require specific integer reasoning out of scope of psatz. | |||
| 2018-10-08 | Fixes #8672 (ill-formed pattern substitution in notation with "let"). | Hugo Herbelin | |
| 2018-10-08 | Fix #5197, handling of algebraic universes | Matthieu Sozeau | |
| They were allowed to stay in terms in some cases. We now ensure that if an evar is defined as e.g. fun x => Type@{foo}, foo is properly refreshed to be non-algebraic as it could otherwise appear in the term and break the invariant. Also cleanup the implementation of refresh_universes to avoid using a mutable reference and simply rely on the Constr.map smartmap idiom instead. This might have compatibility issues, e.g. in HoTT where maybe more non-algebraic proxy universes could be generated, we'll see. For the bug report proper, there is a lack of bidirectional type-checking that makes the initial definition fail (there's a non-canonical choice of dependency if we don't consider the typing constraint). With the Program bidir hint it passes. | |||
| 2018-10-08 | Merge PR #8630: Some cleaning in the test suite | Enrico Tassi | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite