| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-23 | Linter: do not lint untracked files. | Gaëtan Gilbert | |
| 2017-11-23 | Merge PR #6200: Remove pidentref grammar entry. | Maxime Dénès | |
| 2017-11-23 | Merge PR #1092: [stm] [doc] Add some documentation to obscure AsyncTaskQueue | Maxime Dénès | |
| 2017-11-23 | Merge PR #6123: Nix file | Maxime Dénès | |
| 2017-11-23 | Merge PR #6189: Disable whitespace linter for .out files. | Maxime Dénès | |
| 2017-11-23 | Merge PR #6187: Check findlib version in configure (fix #4270). | Maxime Dénès | |
| 2017-11-23 | Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag. | Maxime Dénès | |
| 2017-11-21 | Merge PR #6173: [printing] Deprecate all printing functions accessing the ↵ | Maxime Dénès | |
| global proof. | |||
| 2017-11-21 | [stm] [doc] Add some documentation to AsyncTaskQueue API | Emilio Jesus Gallego Arias | |
| As a bonus we remove some trailing whitespace, and implement a couple of hints suggested in the discussion. | |||
| 2017-11-21 | [printing] Deprecate all printing functions accessing the global proof. | Emilio Jesus Gallego Arias | |
| We'd like to handle proofs functionally we thus recommend not to use printing functions without an explicit context. We also adapt most of the code, making more explicit where the printing environment is coming from. An open task is to refactor some code so we gradually make the `Pfedit.get_current_context ()` disappear. | |||
| 2017-11-21 | Merge PR #6185: [parser] Remove unnecessary statically initialized hook. | Maxime Dénès | |
| 2017-11-21 | Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API. | Maxime Dénès | |
| 2017-11-21 | Merge PR #6178: Have the coq_makefile timing test-suite print more | Maxime Dénès | |
| 2017-11-21 | Merge PR #6168: Add Equations to CI | Maxime Dénès | |
| 2017-11-21 | Merge PR #6113: Extra work on ltac printing: fixing #5787, some parentheses | Maxime Dénès | |
| 2017-11-20 | Fixes #5787 (printing of "constr:" lost in the move of constr to Generic). | Hugo Herbelin | |
| Was broken since 8.6. | |||
| 2017-11-20 | Remove pidentref grammar entry. | Gaëtan Gilbert | |
| Replaced by ident_decl in #688. | |||
| 2017-11-20 | Disable whitespace linter for .out files. | Gaëtan Gilbert | |
| 2017-11-20 | Check findlib version in configure (fix #4270). | Gaëtan Gilbert | |
| 2017-11-20 | Merge PR #6188: Rename coq-inferior.el -> inferior-coq.el to match provided ↵ | Maxime Dénès | |
| feature. | |||
| 2017-11-20 | Merge PR #6184: [lib] Minor pending cleanup to consolidate helper function. | Maxime Dénès | |
| 2017-11-20 | Merge PR #6183: [plugins] Prepare plugin API for functional handling of state. | Maxime Dénès | |
| 2017-11-20 | Merge PR #6166: Fix regression in treating Defined as defined | Maxime Dénès | |
| 2017-11-20 | Merge PR #6163: [dev] Remove deprecation warning from `base_include` | Maxime Dénès | |
| 2017-11-20 | Merge PR #6161: Fix micromega.ml to match generated file and enforce match ↵ | Maxime Dénès | |
| in make. | |||
| 2017-11-20 | Add Equations to CI | Matthieu Sozeau | |
| 2017-11-20 | Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 ↵ | Maxime Dénès | |
| (clause "where" with implicit arguments) | |||
| 2017-11-20 | Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵ | Maxime Dénès | |
| unbound rel | |||
| 2017-11-19 | Fix #5790: make Hint Resolve <- respect univ polymorphism flag. | Gaëtan Gilbert | |
| 2017-11-19 | Rename coq-inferior.el -> inferior-coq.el to match provided feature. | Gaëtan Gilbert | |
| Fixes #4988. | |||
| 2017-11-19 | [parser] Remove unnecessary statically initialized hook. | Emilio Jesus Gallego Arias | |
| Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to put any pattern in binders, prefixed by a quote."] its current placement as well as the hook don't make a lot of sense. In particular, they prevent parts of Coq working without linking the parser. To this purpose, we need to consolidate the `Constrexpr` utilities. While we are at it we do so and remove the `Topconstr` module which is fully redundant with `Constrexpr_ops`. | |||
| 2017-11-19 | [plugins] Prepare plugin API for functional handling of state. | Emilio Jesus Gallego Arias | |
| To this purpose we allow plugins to register functions that will modify the state. This is not used yet, but will be used soon when we remove the global handling of the proof state. | |||
| 2017-11-19 | Remove branch on caml version >= 3.10 from configure. | Gaëtan Gilbert | |
| We require 4.02.3. | |||
| 2017-11-19 | [lib] Minor pending cleanup to consolidate helper function. | Emilio Jesus Gallego Arias | |
| While we are at it we refactor a few special cases of the helper. | |||
| 2017-11-19 | [vernac] Increase table size. | Emilio Jesus Gallego Arias | |
| As of Nov 2017, the standard number of entries is 85, it easily goes up with some other plugins, so 211 seems like a good compromise. | |||
| 2017-11-19 | [proof] Attempt to deprecate some V82 parts of the proof API. | Emilio Jesus Gallego Arias | |
| I followed what seems to be the intention of the code, with the original intention of remove the global imperative proof state. However, I fully fail to see why the new API is better than the old one. In fact the opposite seems the contrary. Still big parts of the "new proof engine" seem unfinished, and I'm afraid I am not the right person to know what direction things should take. | |||
| 2017-11-17 | Have the coq_makefile timing test-suite print more | Jason Gross | |
| This should help debug things like https://github.com/coq/coq/issues/5675#issuecomment-345324924 if they ever show up again. | |||
| 2017-11-16 | Merge PR #6160: Fix gitlab for 4.06 | Maxime Dénès | |
| 2017-11-16 | Merge PR #6148: [api] Another large deprecation, `Nameops` and friends. | Maxime Dénès | |
| 2017-11-16 | Merge PR #6132: Fixes #6129 (declaration of coercions made compatible with ↵ | Maxime Dénès | |
| local definitions) | |||
| 2017-11-16 | Merge PR #6104: Fixing encoding in coqdoc output tests. | Maxime Dénès | |
| 2017-11-16 | Merge PR #6023: Use GHC.Base.Any for compatibility with GHC 8.2 | Maxime Dénès | |
| 2017-11-16 | Fix micromega.ml to match generated file and enforce match in make. | Gaëtan Gilbert | |
| Mismatch probably caused by c5aca4005. | |||
| 2017-11-15 | Fix regression in treating Defined as defined | Tej Chajed | |
| Fixes #6165. | |||
| 2017-11-15 | [dev] Remove deprecation warning from `base_include` | Emilio Jesus Gallego Arias | |
| The warning created problems as OCaml restored the color printing tags when printing it, so users doing `Drop` and then `go ()` got color printing back after the warning. We should guard the console on `Drop` better, but this requires some (much needed) refactoring work in the toplevel. | |||
| 2017-11-15 | Fix gitlab for 4.06 | Gaëtan Gilbert | |
| 2017-11-15 | Fix #5761: cbv on undefined evars under binders produces unbound rel | Gaëtan Gilbert | |
| When an evar is undefined we need to substitute inside the evar instance. With help from @herbelin and @psteckler to identify the issue from a large test case. | |||
| 2017-11-15 | Fixing printing of tactics encapsulated as tacarg with Tacexp. | Hugo Herbelin | |
| We preserve the level instead of resetting it at level 0. Probably it would be the same as giving level ltop since Tacexp apparently comes only from using a tactic in an Ltac "let", which is where I observed a problem. | |||
| 2017-11-15 | Using "l" printer for glob_constr, like for constr. | Hugo Herbelin | |
| This is to avoid excessive parentheses, in particular when printing "constr:()" in "Print Ltac f". | |||
| 2017-11-15 | Merge PR #6147: Change OCAMLRUNPARAM warning to mention OCaml 4.06 | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |