| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-12-14 | Update pinned nixpkgs to use Dune 1.6. | Théo Zimmermann | |
| 2018-12-13 | [dune] [doc] Support for building the reference manual with Dune. | Emilio Jesus Gallego Arias | |
| This is a reduced version of #8503 as to provide a way to build the reference manual with Dune. Dune 1.6 supports (experimentally) directories as targets, thus we introduce a rule that will call `sphinx` to build the manual. This only provides build, however generation of `.install` rules is not done, it will be hopefully addressed in #8503. Note that we set `expire: 1 month` for all the artifacts we build with Dune. IMHO this makes most sense as not to abuse Gitlab's hosting, however of course we could consider a different deployment strategy if wanted. | |||
| 2018-12-13 | Merge PR #9032: checker: check inductive types by roundtrip through the kernel. | Pierre-Marie Pédrot | |
| 2018-12-13 | Merge PR #9167: Fixes #9166: no deprecation warning on aliases used as ↵ | Pierre-Marie Pédrot | |
| pattern variables | |||
| 2018-12-13 | Merge PR #9169: [rtauto] [auto] Use new proof engine. | Pierre-Marie Pédrot | |
| 2018-12-13 | Merge PR #9217: [ci] [appveyor] Temporally disable test suite on Appveyor. | Gaëtan Gilbert | |
| 2018-12-13 | Merge PR #9196: Document the deprecation of hint declaration withou database ↵ | Maxime Dénès | |
| in refman. | |||
| 2018-12-13 | Merge PR #8096: Higher-level libobject API for objects with fixed scopes | Enrico Tassi | |
| 2018-12-13 | [ci] [appveyor] Temporally disable test suite on Appveyor. | Emilio Jesus Gallego Arias | |
| Hopefully we will re-enable it back soon, I am preparing a refactoring that should make it more robust w.r.t paths and changes on Windows which will enable to use a faster build system. But now it is timing out 100% of the times [due to #8655] so it is not useful. | |||
| 2018-12-12 | Merge PR #9101: Fix 8922 again | Hugo Herbelin | |
| 2018-12-12 | Merge PR #9087: Add CI job building stdlib with `async-proofs on` | Emilio Jesus Gallego Arias | |
| 2018-12-12 | Higher-level libobject API for objects with fixed scopes | Maxime Dénès | |
| 2018-12-12 | checker: check inductive types by roundtrip through the kernel. | Gaëtan Gilbert | |
| 2018-12-12 | [rtauto] [auto] Use new proof engine. | Emilio Jesus Gallego Arias | |
| 2018-12-12 | Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation` | Hugo Herbelin | |
| 2018-12-12 | Fixes #9166 (no warning on pattern variables named like a deprecated alias). | Hugo Herbelin | |
| 2018-12-12 | Avoid Fixpoint without struct nor body in stdlib | Maxime Dénès | |
| As reported in #9060, the STM does not handle such constructions properly. They are anyway fragile, for example Guarded reports a failure if run at the end of the scripts, so this patch is an improvement. | |||
| 2018-12-12 | Add CI job building stdlib with `-async-proofs on` | Maxime Dénès | |
| 2018-12-12 | User flags for coqtop/coqc in Makefile and CI build template | Maxime Dénès | |
| 2018-12-12 | Merge PR #8974: Fix mod_subst wrt universe polymorphism | Maxime Dénès | |
| 2018-12-12 | Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix ↵ | Maxime Dénès | |
| comments. | |||
| 2018-12-11 | Add missing formatting. | Théo Zimmermann | |
| 2018-12-11 | Merge PR #9197: Fixing imports in debug printers: gramlib depends on Loc ↵ | Emilio Jesus Gallego Arias | |
| which is in lib.cma | |||
| 2018-12-11 | Merge PR #8655: Test suite: use coqc and then coqchk | Enrico Tassi | |
| 2018-12-11 | Merge PR #9155: Fix race condition triggered by fresh universe generation | Enrico Tassi | |
| 2018-12-11 | Fixing imports in debug printers: gramlib depends on Loc which is in lib.cma. | Hugo Herbelin | |
| 2018-12-11 | Document the deprecation of hint declaration withou database in refman. | Théo Zimmermann | |
| Follow-up of #8987. | |||
| 2018-12-11 | Merge PR #9151: [dune] Teach coq_dune about `.glob` and `.aux` files. | Théo Zimmermann | |
| 2018-12-10 | Fix Invalid_argument in List.iter2 | Jim Fehrle | |
| 2018-12-10 | For diffs, return exactly the characters that make up STRING and FIELD tokens | Jim Fehrle | |
| 2018-12-10 | Fix #9091: don't show deleted compacted hypotheses twice in diff | Jim Fehrle | |
| 2018-12-10 | Treat unmatched goals as new for diffs (highlighted) | Jim Fehrle | |
| Improve debug output | |||
| 2018-12-10 | [test-suite] Fail when the checker fails | Vincent Laporte | |
| 2018-12-10 | [test-suite] Run `coqchk` on most test cases | Vincent Laporte | |
| 2018-12-10 | [dune] Teach coq_dune about `.glob` and `.aux` files. | Emilio Jesus Gallego Arias | |
| This is a required step in order to be able to call `coqdoc` an generate the documentation of the stdlib, and also useful for other uses such as the asynchronous engine. | |||
| 2018-12-10 | Merge PR #9145: Do so that an error message follows the "Error:" header on ↵ | Emilio Jesus Gallego Arias | |
| the same line | |||
| 2018-12-10 | Merge PR #9077: Rename generated directory gramlib__pack -> gramlib/.pack | Emilio Jesus Gallego Arias | |
| 2018-12-10 | Merge PR #9177: add relation-algebra to CI test suite | Gaëtan Gilbert | |
| 2018-12-10 | Merge PR #9106: [dune] Install coq libraries in `%{lib_root}/coq` instead of ↵ | Vincent Laporte | |
| in `lib | |||
| 2018-12-10 | Merge PR #7221: The usual order of strings. | Hugo Herbelin | |
| 2018-12-09 | fix copy-paste error in CI_ARCHIVEURL | Christian Doczkal | |
| 2018-12-09 | add relation-algebra to CI test suite | Christian Doczkal | |
| 2018-12-09 | [doc] Enable Warning 50 [incorrect doc comment] and fix comments. | Emilio Jesus Gallego Arias | |
| This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :) | |||
| 2018-12-08 | [dune] Install coq libraries in `%{lib_root}/coq` instead of `lib` | Emilio Jesus Gallego Arias | |
| This is what the native Dune Coq version already does, but it is a problem for Coq Dune too as noted by @vgbl. | |||
| 2018-12-08 | Do so that an error message follows the "Error:" header on the same line. | Hugo Herbelin | |
| 2018-12-07 | Merge PR #8811: EConstr-aware functions to produce kernel entries | Pierre-Marie Pédrot | |
| 2018-12-06 | Merge PR #9140: [ci] Add four color theorem proof to CI | Gaëtan Gilbert | |
| 2018-12-06 | Revise API for global universes. | Gaëtan Gilbert | |
| Rename Univ.Level.{Qualid -> UGlobal}, remove Univ.Level.Id. Remove the ability to split the argument of `Univ.Level.Level` into a dirpath*int pair (except by going through string hacks like detyping/pretyping(/funind) does). Id.of_string_soft to turn unnamed universes into qualid is pushed up to detyping. (TODO some followup PR clean up more) This makes it pointless to have an opaque type for ints in Univ.Level: it would only be used as argument to Univ.Level.UGlobal.make, ie ~~~ open Univ.Level let x = UGlobal.make dp (Id.make n) (* vs *) let x = UGlobal.make dp n ~~~ Remaining places which create levels from ints are various hacks (eg the dummy in inductive.ml, the Type.n universes in ugraph sort_universes) and univgen. UnivGen does have an opaque type for ints used as univ ids since they get manipulated by the stm. NB: build breaks due to ocamldep issue if UGlobal is named Global instead. | |||
| 2018-12-06 | High level functions to produce kernel entries from econstr. | Gaëtan Gilbert | |
| 2018-12-06 | Evarutil.finalize: combine minimize, to_constr and restrict. | Gaëtan Gilbert | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |