aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-13Generate type-specific code for is_accu in native compilation of fixpoints.Pierre-Marie Pédrot
This is much more efficient than using Nativevalues.is_accu function which incurs a lot of irrelevant checks on its argument.
2018-07-13Store the {struct} inductive type in native fixpoint AST.Pierre-Marie Pédrot
2018-07-13Pass a proper environment to Nativelambda.lambda_of_constr.Pierre-Marie Pédrot
No need to roll up a new data structure when Environment has O(log n) add and lookup of rel definitions.
2018-07-12Merge PR #7907: Tactic deprecation machineryPierre-Marie Pédrot
2018-07-12Merge PR #8051: Clean-up user-overlays folder.Emilio Jesus Gallego Arias
2018-07-12Clean-up user-overlays folder.Théo Zimmermann
2018-07-12Merge PR #7871: [ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Gaëtan Gilbert
2018-07-12Tactic deprecation machineryMaxime Dénès
We make it possible to deprecate tactics defined by `Ltac`, `Tactic Notation` or ML. For the first two variants, we anticipate the syntax of attributes: `#[deprecated(since = "XX", note = "YY")]` In ML, the syntax is: ``` let reflexivity_depr = let open CWarnings in { since = "8.5"; note = "Use admit instead." } TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] END ``` A warning is shown at the point where the tactic is used (either a direct call or when defining another tactic): Tactic `foo` is deprecated since XX. YY YY is typically meant to be "Use bar instead.".
2018-07-11[ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Emilio Jesus Gallego Arias
- We update the OCaml version used in the base CI image. - Windows / OSX image building is also updated to use newer OCaml. - We also update Dune to 1.0.0.
2018-07-11Merge PR #7998: [coqpp] Move to its own directory.Pierre-Marie Pédrot
2018-07-11Merge PR #8035: Fix #8033: Tactic assert-suceeds has a typo in its name in ↵Théo Zimmermann
the manual
2018-07-11Merge PR #8021: Get rid of horrendous hack limiting the size of parsed integersPierre-Marie Pédrot
2018-07-11Merge PR #8002: make-both-single-timing-files: fix --sort-by=diffJason Gross
2018-07-11Merge PR #7898: Remove camlp4 remainsEmilio Jesus Gallego Arias
2018-07-11[coqpp] Move to its own directory.Emilio Jesus Gallego Arias
Coqpp has nothing to do with `grammar`, we thus place it in its own directory, which will prove convenient in more modular build systems. Note that we add `coqpp` to the list of global includes, we could have indeed added some extra rules, but IMHO not worth it as hopefully proper containment will be soon checked by Dune.
2018-07-11Merge PR #7984: Compile `coqpp` inside the `bin/` folder and make it ↵Emilio Jesus Gallego Arias
available after installation
2018-07-11Merge PR #8031: Remove auto-retry in GitLab CI now that @coqbot is handling it.Emilio Jesus Gallego Arias
2018-07-10Compile coqpp inside the bin/ folder and make it available after installation.Pierre-Marie Pédrot
2018-07-10Merge PR #8036: [travis] Remove even more jobs.Emilio Jesus Gallego Arias
2018-07-10Merge PR #8034: [travis] Try to workaround the repeated APT failures by ↵Emilio Jesus Gallego Arias
using Jason Gross's suggestion.
2018-07-10[travis] Remove even more jobs.Théo Zimmermann
Users who want to test external projects should be encouraged to activate GitLab CI as is documented in dev/ci/README.md.
2018-07-10fixed typo for assert_suceedcharguer
2018-07-10[travis] Try to workaround the repeated APT failures by using Jason Gross's ↵Théo Zimmermann
suggestion.
2018-07-10Remove auto-retry in GitLab CI now that @coqbot is handling it.Théo Zimmermann
2018-07-10Merge PR #7899: My recent improvements to the backport script.Maxime Dénès
2018-07-10Merge PR #7983: Turn a dead branch into an assertion failure in VM reification.Maxime Dénès
2018-07-10Merge PR #8028: Fix a few typosThéo Zimmermann
2018-07-10Merge PR #8025: Fix rst syntax for `quote ident {ident}`Théo Zimmermann
2018-07-10Add new options --no-conflict and --no-signature-check to backport script.Théo Zimmermann
2018-07-10Fix typo in doc/proof-engine/tactics.rst.whitequark
2018-07-10Fix typo in Init.Logic.whitequark
2018-07-09Merge PR #7920: Generic syntax for attributesMaxime Dénès
2018-07-09Fix rst syntax for `quote ident {ident}`Joachim Breitner
2018-07-09Merge PR #7884: Fix #5719: Uncaught exception Invalid_argument.Matthieu Sozeau
2018-07-08Merge PR #8015: Output UTF-8 explicitly in timing toolsJason Gross
2018-07-08Get rid of horrendous hack limiting the size of parsed integersMaxime Dénès
2018-07-08Merge PR #7985: Remove letouzey from CODEOWNERS since he left the Coq ↵Maxime Dénès
organization.
2018-07-08Merge PR #8020: Modify URLs in xml-protocol.mdThéo Zimmermann
2018-07-08Modify URLs in xml-protocol.mdRin Arakaki
2018-07-08Modify URLs in xml-protocol.mdRin Arakaki
2018-07-08Merge PR #7843: Remove Emacs modesMaxime Dénès
2018-07-08Mention the removal of Emacs modes in CHANGES.Théo Zimmermann
2018-07-08Remove Emacs modes.Théo Zimmermann
They are not used anymore. People should use Proof-General (and optionally Company-Coq) instead.
2018-07-07make diff sort by difference, not absolute differenceRalf Jung
2018-07-07make-both-single-timing-files: fix --sort-by=diffRalf Jung
2018-07-07Output UTF-8 explicitly in timing toolsJasper Hugunin
2018-07-07Merge PR #7921: Archive the `gallina` toolMaxime Dénès
2018-07-07Add an overlay.Pierre-Marie Pédrot
2018-07-07Merge PR #7956: Rebuild coqtop$(EXE) in "make coqbinaries" in addition to ↵Enrico Tassi
coqtop.opt$(EXE).
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
We deprecate the corresponding functions in Pcoq.Gram. The motivation is that the Gram module is used as an argument to Camlp5 functors, so that it is not stable by extension. Enforcing that its type is literally the one Camlp5 expects ensures robustness to extension statically. Some really internal functions have been bluntly removed. It is unlikely that they are used by external plugins.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:15:52 +0000