aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Merge PR #7249: Cleaning, documentation, uniformisation of the Coq extension ↵Gravatar Pierre-Marie Pédrot2018-06-04
|\ | | | | | | of List
* \ Merge PR #7619: Mention test-suite in PR templateGravatar Maxime Dénès2018-06-04
|\ \
* \ \ Merge PR #7648: Indicate in the doc that clearbody can take several identsGravatar Maxime Dénès2018-06-04
|\ \ \
* \ \ \ Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.Gravatar Maxime Dénès2018-06-04
|\ \ \ \
* \ \ \ \ Merge PR #7657: Fix a couple typos in deprecation messagesGravatar Pierre-Marie Pédrot2018-06-04
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7640: Small refactoring to clarify make_local_hint_db.Gravatar Pierre-Marie Pédrot2018-06-04
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7649: Remove some dead code in class_tactics.mlGravatar Pierre-Marie Pédrot2018-06-04
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7682: Fixes #7641: more detailed message about disjunctive ↵Gravatar Emilio Jesus Gallego Arias2018-06-03
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | patterns with different variables
* \ \ \ \ \ \ \ \ Merge PR #7689: configure: fix warning printingGravatar Emilio Jesus Gallego Arias2018-06-03
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #7637: Fix an outdated comment refering to lib/dnet.mliGravatar Pierre-Marie Pédrot2018-06-03
|\ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | configure: fix warning printingGravatar Gaëtan Gilbert2018-06-03
| |/ / / / / / / / / |/| | | | | | | | |
| | | | | | | | | * Further sharing in CList.Gravatar Hugo Herbelin2018-06-03
| | | | | | | | | |
| | | | | | | | | * Cleaning, documentation, uniformisation of the Coq extension of List.Gravatar Hugo Herbelin2018-06-03
| |_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Still some discrepancies though. E.g.: - some functions taking an equality as arguments have suffix `_f` but not all; - the functions possibly raising an error have still different kinds of failure (Failure, Invalid_argument, Not_found or IndexOutOfRange, and when in the first two cases, with no unique rules in the style of the associated string - we thus avoid to document the exact string used). There are a few semantics changes: - skipn_at_least now raises a `Failure` if its argument is negative; - map3 raises an Invalid_argument "List.map3" rather than Invalid_argument "map3" and similarly for map4 - internally, map3 and map4 are now tail-recursive (by uniformity); - internally, split3 and combine3 are now tail-recursive (by uniformity); - filter is now "smart" by default and smartfilter is deprecated; - smartmap is now tail-recursive by default.
* | | | | | | | | Merge PR #7683: [lib] Fix wrong deprecation annotations.Gravatar Pierre-Marie Pédrot2018-06-03
|\ \ \ \ \ \ \ \ \
| | | * | | | | | | Fixes #7641: more detailed message for disjunctive patterns with different vars.Gravatar Hugo Herbelin2018-06-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Could still be made more detailed with more time.
* | | | | | | | | | Merge PR #7656: CI for QuickChick and ext-libGravatar Emilio Jesus Gallego Arias2018-06-03
|\ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | Update .gitlab to use newer ocamlGravatar Leonidas Lampropoulos2018-06-02
| | | | | | | | | | |
| | * | | | | | | | | [lib] Fix wrong deprecation annotations.Gravatar Emilio Jesus Gallego Arias2018-06-03
| |/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Introduced in #7177
* | | | | | | | | | Merge PR #7681: Fixes #7636: location missing on deprecated compatibility ↵Gravatar Emilio Jesus Gallego Arias2018-06-03
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | notations.
| | * | | | | | | | | QuickChick CIGravatar Leonidas Lampropoulos2018-06-02
| |/ / / / / / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR #7680: [ci] Expose updated `OCAMLPATH` for CI users.Gravatar Gaëtan Gilbert2018-06-02
|\ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / |/| | | | | | | | |
| | * | | | | | | | Fixes #7636: location missing on deprecated compatibility notations.Gravatar Hugo Herbelin2018-06-02
| |/ / / / / / / / |/| | | | | | | |
| * | | | | | | | [ci] Expose updated `OCAMLPATH` for CI users.Gravatar Emilio Jesus Gallego Arias2018-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is needed for CI packages that use `META.coq` such as in https://github.com/coq/coq/pull/7656 .
* | | | | | | | | Merge PR #7234: Reduce circular dependency constants <-> projectionsGravatar Maxime Dénès2018-06-01
|\ \ \ \ \ \ \ \ \ | |/ / / / / / / / |/| | | | | | | |
* | | | | | | | | Merge PR #7570: [api] Move `Constrexpr` to the `interp` module.Gravatar Maxime Dénès2018-06-01
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #7537: Improve the Gallina chapter of the reference manual.Gravatar Maxime Dénès2018-06-01
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #7606: Allow more than one signature and name per Sphinx objectGravatar Maxime Dénès2018-06-01
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7660: Add codeowner for timing python scriptsGravatar Maxime Dénès2018-06-01
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | * | Merge two clearbody docsGravatar Théo Winterhalter2018-06-01
| | | | | | | | | | | | |
* | | | | | | | | | | | | Merge PR #7652: Explicitly require python2 in python scripts in tools/Gravatar Jason Gross2018-05-31
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | | | | Add codeowner for timing python scriptsGravatar Jason Gross2018-05-31
| |/ / / / / / / / / / / / |/| | | | | | | | | | | |
| | | | | | | | | * | | | Fix a couple typos in deprecation messagesGravatar Armaël Guéneau2018-05-31
| | | | | | | | | | | | |
* | | | | | | | | | | | | Merge PR #7401: Automatically run alienclean before compiling.Gravatar Enrico Tassi2018-05-31
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | |
| | * | | | | | | | | | | Explicitly require python2 in python scripts in tools/Gravatar Armaël Guéneau2018-05-31
| |/ / / / / / / / / / / |/| | | | | | | | | | |
| | | | | | | * | | | | Remove some dead code in class_tactics.mlGravatar Armaël Guéneau2018-05-31
| |_|_|_|_|_|/ / / / / |/| | | | | | | | | |
| | | | * | | | | | | [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously to this patch, `Notation_term` contained information about both parsing and notation interpretation. We split notation grammar to a file `parsing/notation_gram` as to make `interp/` not to depend on some parsing structures such as entries.
| | | | * | | | | | | [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-05-31
| |_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Continuing the interface cleanup we place `Constrexpr` in the internalization module, which is the one that eliminates it. This slims down `pretyping` considerably, including removing the `Univdecls` module which existed only due to bad dependency ordering in the first place. Thanks to @ Skyskimmer we also remove a duplicate `univ_decl` definition among `Misctypes` and `UState`. This is mostly a proof of concept yet as it depends on quite a few patches of the tree. For sure some tweaks will be necessary, but it should be good for review now. IMO the tree is now in a state where we can could easy eliminate more than 10 modules without any impact, IMHO this is a net saving API-wise and would help people to understand the structure of the code better.
* | | | | | | | | | Merge PR #6969: [api] Remove functions deprecated in 8.8Gravatar Maxime Dénès2018-05-31
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | * | Indicate in the doc that clearbody can take several identsGravatar Théo Winterhalter2018-05-31
| | | | | | | | | | |
* | | | | | | | | | | Merge PR #7564: Move interning the [hint_pattern] outside the Typeclasses hooks.Gravatar Emilio Jesus Gallego Arias2018-05-31
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | |
| | | | | | * | | | | Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
| |_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead of having the projection data in the constant data we have it independently in the environment.
* | | | | | | | | | Merge PR #7578: Allow make clean to work on a fresh cloneGravatar Enrico Tassi2018-05-31
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #7639: Makefile: fix undefined NATIVEFILES when -native-compute noGravatar Enrico Tassi2018-05-31
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7633: [Makefile] New target “install-merlin”Gravatar Enrico Tassi2018-05-31
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | * | | | | | | | | Move interning the [hint_pattern] outside the Typeclasses hooks.Gravatar Gaëtan Gilbert2018-05-30
| |_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Close #7562. [api] move hint_info ast to tactics.
| | | | * | | | | | | | [api] Remove deprecated objects in engine / interp / libraryGravatar Emilio Jesus Gallego Arias2018-05-30
| | | | | | | | | | | |
| | | | * | | | | | | | [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove most of what was deprecated in `Term`. Now, `intf` and `kernel` are almost deprecation-free, tho I am not very convinced about the whole `Term -> Constr` renaming but I'm afraid there is no way back. Inconsistencies with the constructor policy (see #6440) remain along the code-base and I'm afraid I don't see a plan to reconcile them. The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a good idea as someone added a `List` module inside it.
| | | | * | | | | | | | [api] Remove deprecated aliases from `Names`.Gravatar Emilio Jesus Gallego Arias2018-05-30
| | | | | | | | | | | |
| | | | * | | | | | | | [api] Reintroduce `Names.global_reference` aliasGravatar Emilio Jesus Gallego Arias2018-05-30
| |_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Due to a bad interaction between PRs, the `Names.global_reference` alias was removed in 8.9, where it should disappear in 8.10. The original PR #6156 deprecated the alias in `Libnames`.
* | | | | | | | | | | Merge PR #7260: Fix #6951: Unexpected error during scheme creation.Gravatar Maxime Dénès2018-05-30
|\ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 03:47:49 +0000