| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-09 | Merge PR #8601: Move bound universe names to abstract contexts | Gaëtan Gilbert | |
| 2018-11-09 | Add a test for bug #8939. | Pierre-Marie Pédrot | |
| 2018-11-09 | Use arrays of names instead of lists in abstract universe names. | Pierre-Marie Pédrot | |
| There is little point in having a list, as there is virtually no sharing nor expansion of bound universe names. This representation is thus more compact. | |||
| 2018-11-09 | Adding universe names to polymorphic entry instances. | Pierre-Marie Pédrot | |
| 2018-11-08 | Standardize handling of Automatic Introduction. | Jasper Hugunin | |
| This fixes #8791. We explicitly specify for intro the names of binders which are given by the user. This still can suffer from spurious collisions, see #8819. | |||
| 2018-11-07 | Revert "Do not allow spliting in res_pf, this is reserved for pretyping" | Enrico Tassi | |
| This reverts commit 8d8200d4bff3ffc44efc51ad44dccee9eb14ec6a. Fix #7936 # Conflicts: # proofs/clenvtac.ml | |||
| 2018-11-06 | Merge PR #8556: [ssr] use tclDISPATCH for IPatDispatch (fix #8544) | Maxime Dénès | |
| 2018-11-05 | Merge PR #8515: Command driven attributes | Pierre-Marie Pédrot | |
| 2018-11-05 | Merge PR #8870: Pass native and VM flags to the kernel through environment | Pierre-Marie Pédrot | |
| 2018-11-05 | Merge PR #8874: Fix #8873: coqchk on inductive with letin parameter | Pierre-Marie Pédrot | |
| 2018-11-05 | Merge PR #8882: Fix #8881: validate fails to use inductive equivalence in ↵ | Pierre-Marie Pédrot | |
| case_info | |||
| 2018-11-05 | Pass native and VM flags to the kernel through environment | Maxime Dénès | |
| The kernel no longer has to read the configure flag, its value can now be overriden by a coqtop/coqc argument, and more generally is easier to set from a toplevel (such as the checker). We also add a `-bytecode-compiler` flag. Fixes #4607 | |||
| 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-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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite