| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-09-01 | Changelog: more accurate on uncons | Yishuai Li | |
| 2019-09-01 | Vectors: lemmas about uncons and splitAt | Yishuai Li | |
| Co-authored-by: Konstantinos Kallas <konstantinos.kallas@hotmail.com> | |||
| 2019-08-30 | Merge PR #10714: Solve universe error with SSR 'rewrite !term' | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-08-29 | Solve universe error with SSR 'rewrite !term' | Andreas Lynge | |
| 2019-08-29 | Merge PR #10693: Create a maintainer team for the contributing process files. | Maxime Dénès | |
| Reviewed-by: ejgallego Reviewed-by: maximedenes | |||
| 2019-08-29 | Merge PR #10674: [declare] Move proof_entry type to declare, put interactive ↵ | Pierre-Marie Pédrot | |
| proof data on top of declare. Reviewed-by: ppedrot | |||
| 2019-08-29 | Merge PR #10660: [cleanup] Replace uses of UserError constructor, clarify ↵ | Pierre-Marie Pédrot | |
| exception names Reviewed-by: ppedrot | |||
| 2019-08-29 | Merge PR #9066: [parsing] Move pcoq-specific parts in extend to pcoq. | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-08-29 | Merge PR #10703: Make Bool.eqb_spec transparent | Hugo Herbelin | |
| Reviewed-by: herbelin Reviewed-by: ppedrot | |||
| 2019-08-29 | Merge PR #10643: [glob/aux files] Remove undocumented Stdout dump, cleanup ↵ | Hugo Herbelin | |
| flags. Ack-by: SkySkimmer Ack-by: gares Reviewed-by: herbelin | |||
| 2019-08-28 | Merge PR #10488: Simplify picking between uint63_63.ml and uint63_31.ml + ↵ | Enrico Tassi | |
| makefile fixes Reviewed-by: ejgallego Reviewed-by: vbgl | |||
| 2019-08-28 | Merge PR #10646: Recommend assigning an issue before fixing a bug. | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-08-28 | Merge PR #10709: Add missing entry to the contributing guide TOC. | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-08-27 | [declare] Use entry constructor instead of low-level record. | Emilio Jesus Gallego Arias | |
| Non-delayed entries can be done with the current constructor, delayed ones will require more work. | |||
| 2019-08-27 | Merge PR #10680: Tauto: use Coqlib to locate “not” and “NNPP” | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-08-27 | [declare] Move proof_entry type to declare, put interactive proof data on ↵ | Emilio Jesus Gallego Arias | |
| top of declare. This PR is a follow up to #10406 , moving the then introduced `proof_entry` type to `Declare`. This makes sense as `Declare` is the main consumer of the entry type, and already provides the constructors for it. This is a step towards making the entry type private, which will allow us to enforce / handle invariants on entry data better. A side-effect of this PR is that now `Proof_global` does depend on `Declare`, not the other way around, but that makes sense given that closing an interactive proof will be a client of declare. Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into tactics due to `abstract`, at some point we may be able to unify all them into a single file in `vernac`. | |||
| 2019-08-27 | [cleanup] Replace uses of UserError constructor, clarify exception names. | Emilio Jesus Gallego Arias | |
| We replace some uses of `raise (UserError ...)` with `CErrors.user_err`, ideally we would like to make the error raising API not depend on the exception themselves, but that's still a long way to go. We also rename the `Timeout` exception as to clarify purpose in the codebase, given that it has 3 different ones as of today. cc: #7560 | |||
| 2019-08-27 | Merge PR #10635: [funind] Port indfun to the new tactic engine. | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-08-27 | Add missing entry to the contributing guide TOC. | Théo Zimmermann | |
| And add links to UI in the browser. | |||
| 2019-08-26 | Tauto: use Coqlib to locate “not” and “NNPP” | Vincent Laporte | |
| 2019-08-26 | Merge PR #10677: coqchk: Cleanup environment manipulation in ↵ | Pierre-Marie Pédrot | |
| check_constant_declaration Reviewed-by: ppedrot | |||
| 2019-08-26 | Merge PR #10696: [lib] [future] Small cleanup of ununsed functions. | Pierre-Marie Pédrot | |
| Reviewed-by: gares Reviewed-by: ppedrot | |||
| 2019-08-26 | [glob/aux files] Remove undocumented Stdout dump, cleanup flags. | Emilio Jesus Gallego Arias | |
| Fixes #10640 We remove the `StdOut` dump target, so now dump will only happen if a file is specified. Indeed, we make the default no to dump, and enable dump only in coqc, moving the option to the `Coqcargs` module. No need for a changes entry as this feature was undocumented, and no use case was given when introduced. Output to feedback must be explicitly enabled by clients / coqidetop, and we have thus also removed the undocumented option `-feedback-glob`. | |||
| 2019-08-26 | [lib] [future] Small cleanup of ununsed functions. | Emilio Jesus Gallego Arias | |
| 2019-08-25 | Make Bool.eqb_spec transparent | Tej Chajed | |
| 2019-08-25 | Changed chmod -w to chmod a-w to avoid error on cygwin | Michael Soegtrop | |
| 2019-08-25 | Merge PR #10632: Prove the completeness of real numbers from logical axiom ↵ | Hugo Herbelin | |
| sig_not_dec Reviewed-by: herbelin | |||
| 2019-08-24 | saner cond_flags in makefile | Gaëtan Gilbert | |
| 2019-08-24 | Simplify picking between uint63_63.ml and uint63_31.ml | Gaëtan Gilbert | |
| - remove the architecture component (we don't do anything arch-specific so it was just a rewording of int_size) - have configure tell the make build system about int_size instead of reimplementing cp As a bonus, add the copyright header to uint63.mli. | |||
| 2019-08-24 | Merge PR #10698: [dune] Migrate static Dune files to Dune 1.10 | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-08-24 | [dune] Migrate static Dune files to Dune 1.10 | Emilio Jesus Gallego Arias | |
| This improves error reporting. Addendum to #10515 | |||
| 2019-08-23 | coqchk: Cleanup environment manipulation in check_constant_declaration | Gaëtan Gilbert | |
| Instead of doing (simplified code) ~~~ocaml let check env kn cb = let flags = env.flags in let env' = set_flags env cb.flags in ... let env = add_constant cb kn (if poly then env else env') in set_flags env flags ~~~ (NB: when not poly env' has only the typing flags different from env) we do ~~~ocaml let check env kn cb = let env = set_flags env cb.flags in ... () let check env kn cb = let () = check env kn cb in add_constant cb kn env ~~~ | |||
| 2019-08-23 | Merge PR #10686: DAG-style pipelines | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2019-08-23 | Merge PR #10665: [api] Move handling of variable implicit data to impargs | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2019-08-23 | [gitlab/ci] Rework stages, always use needs keyword. | Théo Zimmermann | |
| Now everything that does not have any dependencies goes to the first stage. The rest goes to the first stage following all its dependencies. All jobs specifying a dependencies keyword also specify a needs keyword. | |||
| 2019-08-23 | Merge PR #10691: [doc] Fix documentation of schedule-vio | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-08-23 | Create a maintainer team for the contributing process files. | Théo Zimmermann | |
| 2019-08-23 | [doc] Fix documentation of schedule-vio | Emilio Jesus Gallego Arias | |
| Master version of the fix for #10679 | |||
| 2019-08-22 | [gitlab/ci] Do not wait for all builds to finish to run the tests. | Théo Zimmermann | |
| 2019-08-22 | [gitlab/ci] Build Bignums only once. | Théo Zimmermann | |
| We go back to the kind of workflow we had in CircleCI thanks to GitLab 12.2 new needs keyword. | |||
| 2019-08-22 | [gitlab/ci] Deploy sooner thanks to new needs keyword. | Théo Zimmermann | |
| 2019-08-22 | Merge PR #10515: [dune] Move to Dune 1.10, use coq.pp directive. | Théo Zimmermann | |
| Reviewed-by: Zimmi48 Reviewed-by: vbgl | |||
| 2019-08-22 | Merge PR #9062: Delay the computation of frozen evars in legacy unification. | Matthieu Sozeau | |
| Reviewed-by: mattam82 | |||
| 2019-08-22 | [dune] Move to Dune 1.10, use coq.pp directive. | Emilio Jesus Gallego Arias | |
| We use the `(coq.pp ...)` dune directive which will produce correct error messages for `.mlg` files. Unfortunately we cannot yet use the automatic opam generation features of Dune 1.10, as this does require a fully native Dune build. Dune 1.6-1.10 has quite a few other improvements that could be used by Coq, for example for promote modes. I have fixed a couple of documentation issues. `Drop` and `ocamldebug` have been tested in this version. | |||
| 2019-08-21 | Merge PR #10678: [ci] Remove dead code. | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-08-21 | Merge PR #10666: [api] Move `Keys` to pretyping | Enrico Tassi | |
| Reviewed-by: gares Reviewed-by: ppedrot | |||
| 2019-08-20 | [ci] Remove dead code. | Théo Zimmermann | |
| TLC and CPDT are not actually tested. No point in keeping them as if they were. | |||
| 2019-08-20 | Merge PR #10291: Controlling typing flags with commands (no attribute) | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 | |||
| 2019-08-19 | Split ConstructiveRealsLUB and improve comments | Vincent Semeria | |
| 2019-08-19 | Merge PR #10672: Std++, Iris, and Lambda-Rust have moved. | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |