aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-08-29Merge PR #10703: Make Bool.eqb_spec transparentHugo Herbelin
Reviewed-by: herbelin Reviewed-by: ppedrot
2019-08-29Merge PR #10643: [glob/aux files] Remove undocumented Stdout dump, cleanup ↵Hugo Herbelin
flags. Ack-by: SkySkimmer Ack-by: gares Reviewed-by: herbelin
2019-08-28Merge PR #10488: Simplify picking between uint63_63.ml and uint63_31.ml + ↵Enrico Tassi
makefile fixes Reviewed-by: ejgallego Reviewed-by: vbgl
2019-08-28Merge PR #10646: Recommend assigning an issue before fixing a bug.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-08-28Merge PR #10709: Add missing entry to the contributing guide TOC.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-08-27Merge PR #10680: Tauto: use Coqlib to locate “not” and “NNPP”Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-27Merge PR #10635: [funind] Port indfun to the new tactic engine.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-27Add missing entry to the contributing guide TOC.Théo Zimmermann
And add links to UI in the browser.
2019-08-26Tauto: use Coqlib to locate “not” and “NNPP”Vincent Laporte
2019-08-26Merge PR #10677: coqchk: Cleanup environment manipulation in ↵Pierre-Marie Pédrot
check_constant_declaration Reviewed-by: ppedrot
2019-08-26Merge 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-25Make Bool.eqb_spec transparentTej Chajed
2019-08-25Changed chmod -w to chmod a-w to avoid error on cygwinMichael Soegtrop
2019-08-25Merge PR #10632: Prove the completeness of real numbers from logical axiom ↵Hugo Herbelin
sig_not_dec Reviewed-by: herbelin
2019-08-24saner cond_flags in makefileGaëtan Gilbert
2019-08-24Simplify picking between uint63_63.ml and uint63_31.mlGaë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-24Merge PR #10698: [dune] Migrate static Dune files to Dune 1.10Théo Zimmermann
Reviewed-by: Zimmi48
2019-08-24[dune] Migrate static Dune files to Dune 1.10Emilio Jesus Gallego Arias
This improves error reporting. Addendum to #10515
2019-08-23coqchk: Cleanup environment manipulation in check_constant_declarationGaë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-23Merge PR #10686: DAG-style pipelinesGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-08-23Merge PR #10665: [api] Move handling of variable implicit data to impargsGaë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-23Merge PR #10691: [doc] Fix documentation of schedule-vioThéo Zimmermann
Reviewed-by: Zimmi48
2019-08-23[doc] Fix documentation of schedule-vioEmilio 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-22Merge PR #10515: [dune] Move to Dune 1.10, use coq.pp directive.Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: vbgl
2019-08-22Merge 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-21Merge PR #10678: [ci] Remove dead code.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-08-21Merge PR #10666: [api] Move `Keys` to pretypingEnrico 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-20Merge PR #10291: Controlling typing flags with commands (no attribute)Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2019-08-19Split ConstructiveRealsLUB and improve commentsVincent Semeria
2019-08-19Merge PR #10672: Std++, Iris, and Lambda-Rust have moved.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-08-19Merge PR #10671: Remove links to doc artifacts and replace them with the ↵Emilio Jesus Gallego Arias
deployed versions. Reviewed-by: ejgallego
2019-08-19[declare] Use `binding_kind` for implicit kind instead of boolean.Emilio Jesus Gallego Arias
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
We move `binder_kind` to the pretyping AST, removing the last data type in the now orphaned file `Decl_kinds`. This seems a better fit, as this data is not relevant to the lower layers but only used in `Impargs`. We also move state keeping to `Impargs`, so now implicit declaration must include the type. We also remove a duplicated function.
2019-08-19Remove links to doc artifacts and replace them with the deployed versions.Théo Zimmermann
2019-08-19Std++, Iris, and Lambda-Rust have moved.Théo Zimmermann
We update the URLs to the new ones, even if the previous continue to work.
2019-08-19Merge PR #10454: [vernac] Refactor control attributes and fix bug #10452Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2019-08-18[api] Move `Keys` to pretypingEmilio Jesus Gallego Arias
This file is unrelated to library, but to pretyping/unification. This commit, along with others already submitted go towards the goal of `library` containing only the handling of library objects.
2019-08-17Delay the computation of frozen evars in legacy unification.Pierre-Marie Pédrot
This source of slowness has been observed in VST, but it is probably pervasive. Most of the unification problems are not mentioning evars, it is thus useless to compute the set of frozen evars upfront. We also seize the opportunity to reverse the flag, because it is always used negatively.
2019-08-16Merge PR #10663: Fix quoting in 8.9 changelog entry.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-08-16Fix quoting in 8.9 changelog entry.Théo Zimmermann
2019-08-16Fix typing_flags in the checkerSimonBoulier
Now all relevant typing_flags are taken in account by the checker. The different forms of assumptions are now printed by the checker.
2019-08-16Fix Print Assumptions: Inductive types can have unsafe fixpoints orSimonBoulier
type-in-type universes
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:06:38 +0000