aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| |_|_|_|_|_|/ / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | * | | Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Gravatar 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
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7558: [api] Make `vernac/` self-contained.Gravatar Maxime Dénès2018-05-30
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7621: Tactics.introduction: remove dangerous option ~checkGravatar Pierre-Marie Pédrot2018-05-30
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | * | | | | | | | | | | | | | | | Small refactoring to clarify make_local_hint_db.Gravatar Théo Zimmermann2018-05-30
| |_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | * | | | | | | | | | | | | | | | | | | | | Makefile: fix undefined NATIVEFILES when -native-compute noGravatar Gaëtan Gilbert2018-05-30
| |_|_|_|/ / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | * | | | | | | Fix #7113: Program Let Fixpoint in section causes anomalyGravatar Gaëtan Gilbert2018-05-30
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | | | | | Fix an outdated comment refering to lib/dnet.mliGravatar Armaël Guéneau2018-05-30
| | | | | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7593: Don't try to install native compiled files if native-compile ↵Gravatar Maxime Dénès2018-05-29
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | is not set
| | | | * | | | | | | | | | | | | | | | | | | | | Fix #6951: Unexpected error during scheme creation.Gravatar Pierre-Marie Pédrot2018-05-29
| |_|_|/ / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When creating a scheme for bifinite inductive types, we do not create a fixpoint.
* | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7566: Remove a dead old-refman file.Gravatar Maxime Dénès2018-05-29
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7628: [default.nix] Update dependency listGravatar Théo Zimmermann2018-05-29
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7626: Test for #7333 (soundness with VM/native and cofix)Gravatar Théo Zimmermann2018-05-29
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | * | | | | | | | | | | | | | | | | | | | [Makefile] New target “install-merlin”Gravatar Vincent Laporte2018-05-29
| |_|_|_|_|_|/ / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Building this target installs the files that are used by merlin: - .merlin files (.merlin); - bin-annot files (.cmt, .cmti); - source files (.ml, .mli). Plug-in developpers can thus work with an “installed” version of Coq.
| | * | | | | | | | | | | | | | | | | | | | | | | | [default.nix] Adds “ounit” to check dependenciesGravatar Vincent Laporte2018-05-29
| | | | | | | | | | | | | | | | | | | | | | | | | |
| | * | | | | | | | | | | | | | | | | | | | | | | | [default.nix] List “hostname” as a dependencyGravatar Vincent Laporte2018-05-29
| | | | | | | | | | | | | | | | | | | | | | | | | |
| | * | | | | | | | | | | | | | | | | | | | | | | | [default.nix] Use OCaml 4.06Gravatar Vincent Laporte2018-05-29
| | | | | | | | | | | | | | | | | | | | | | | | | |
| | * | | | | | | | | | | | | | | | | | | | | | | | [default.nix] Drop dependency to ocp-indexGravatar Vincent Laporte2018-05-29
| |/ / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7084: [default.nix] Unpin nixpkgsGravatar Théo Zimmermann2018-05-29
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | | | | | | | | | | | | | | | | Add test for #7333: vm_compute segfaults / Anomaly with cofixGravatar Maxime Dénès2018-05-29
| |/ / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7521: Fix soundness bug with VM/native and cofixpointsGravatar Pierre-Marie Pédrot2018-05-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | * | | | | | | | | | | | | | | | | | | | Tactics.introduction: remove dangerous option ~checkGravatar Enrico Tassi2018-05-28
| |_|_|_|/ / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In locally nameless mode (proof mode) names in the context *must* be distinct otherwise the term representation makes no sense.
| | | | | | | | | * | | | | | | | | | | | | | | Improve the last section of the Gallina chapter.Gravatar Théo Zimmermann2018-05-28
| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | | | | | Chapter 1 of the refman compiles without reporting any undocumented object.Gravatar Théo Zimmermann2018-05-28
| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | | | | | Improve sections on (Co)Fixpoint of the Gallina chapter.Gravatar Théo Zimmermann2018-05-28
| | | | | | | | | | | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | | | | | | | | | | Add CHANGES entryGravatar Maxime Dénès2018-05-28
| | | | | | | | | | | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | | | | | | | | | | Fix #7333: vm_compute segfaults / Anomaly with cofixGravatar Maxime Dénès2018-05-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We eta-expand cofixpoints when needed, so that their call-by-need evaluation is correctly implemented by VM and native_compute.
| | | | | | | | | | | * | | | | | | | | | | | | Mention test-suite in PR templateGravatar Jason Gross2018-05-28
| |_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Close #7617
| * | | | | | | | | | | | | | | | | | | | | | Unify pre_env and envGravatar Maxime Dénès2018-05-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We now have only two notions of environments in the kernel: env and safe_env.
| * | | | | | | | | | | | | | | | | | | | | | Remove vm_conv hook and reorganize kernel filesGravatar Maxime Dénès2018-05-28
| | | | | | | | | | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 05:31:05 +0000