aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* An experimental 'Show Extraction' command (grant feature wish #4129)Gravatar Pierre Letouzey2018-03-06
| | | | | | Attempt to extract the current ongoing proof (request by Clément Pit-Claudel on coqdev, and also #4129). Evars are handled as axioms.
* Extraction: switch to EConstr.t as the central type to extract from.Gravatar Pierre Letouzey2018-03-06
| | | | | | | | | | | This is a bit artificial since the extraction normally operates on finished constrs (with no evars). But: - Since we use Retyping quite a lot, switching to EConstr.t allows to get rid of many `EConstr.Unsafe.to_constr (... (EConstr.of_constr ...))` - This prepares the way for a possible extraction of the content of ongoing proofs (a forthcoming `Show Extraction` command, see #4129 )
* Merge PR #6856: travis: elpi needs findlib >= 1.5Gravatar Maxime Dénès2018-03-01
|\
* \ Merge PR #6864: Remove empty, wrongly located, doc file.Gravatar Maxime Dénès2018-03-01
|\ \
* \ \ Merge PR #6861: Typo in the documentation of the `pattern` tacticGravatar Maxime Dénès2018-03-01
|\ \ \
* \ \ \ Merge PR #6850: Fix #6751 trust_file_cache logic was invertedGravatar Maxime Dénès2018-03-01
|\ \ \ \
| | | | * travis: elpi needs findlib >= 1.5Gravatar Enrico Tassi2018-02-28
| | | | |
| | | | * tavis: make the . in pkg.version part of $VERSIONGravatar Enrico Tassi2018-02-28
| | | | |
* | | | | Merge PR #6847: Fix make source-docGravatar Maxime Dénès2018-02-28
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6854: comment "resolvability" bit in Evd.evar_mapGravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6852: [stdlib] move “Require” out of sectionsGravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6853: Add a comment on EConstr.to_constr regarding evar-freeness.Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmasGravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6756: Fix issue with spurious timing test failuresGravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6788: Fixes #6787 (minus sign interpreted by coqdoc as a bullet in ↵Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Ring_theory.v)
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6789: Check whitespace errors per-commit.Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6823: Fixes #6821 (bug in protecting notation printing from ↵Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | infinite eta-expansion)
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6812: Rename release_lexer_state to the more descriptive ↵Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | get_lexer_state.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6752: Remove from CircleCI builds that are already taken care of ↵Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | by Travis.
| | | | | | | | | | | | | | | * Remove empty, wrongly located, doc file.Gravatar Théo Zimmermann2018-02-28
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | |
| | | | | | | | | | | | | | * Typo in the documentation of the `pattern` tacticGravatar Joachim Breitner2018-02-27
| |_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | |
| | | | | | | | | | | * | | comment "resolvability" bit in Evd.evar_mapGravatar Enrico Tassi2018-02-27
| |_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | |
| | | | | | | | | | | | * Fix #6751 trust_file_cache logic was invertedGravatar Gaëtan Gilbert2018-02-27
| |_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Bug introduced by 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54
| | | | | | | | | * | | Add a comment on EConstr.to_constr regarding evar-freeness.Gravatar Pierre-Marie Pédrot2018-02-27
| |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | |
| | | | | | | | | * | [stdlib] move “Require” out of sectionsGravatar Vincent Laporte2018-02-27
| |_|_|_|_|_|_|_|/ / |/| | | | | | | | |
| | | | | | | | | * Use relative path for show_latex_messagesGravatar mrmr19932018-02-27
| | | | | | | | | |
| | | | | | | | | * Use MYCAMLP5LIB instead of undefined MYCAMLP4LIBGravatar mrmr19932018-02-27
| |_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This completes the work of b60906cc3ee3f994babf9cceff2971bd03485f2f
| | | | | | | * | [test-suite] Move sed scripts into bash arraysGravatar Jason Gross2018-02-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/6756/files#r168028764
* | | | | | | | | Merge PR #6543: Update headers and creditsGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6784: New IR in VM: ClambdaGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6819: Document Arguments extra scopes flagGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6803: coqdev.el: add space at the end of compile-commandGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6599: Decimals in preludeGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6745: [ast] Improve precision of Ast location recognition in ↵Gravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | serialization.
| | | | | | | | | | | | * | | | Check whitespace errors per-commit.Gravatar Gaëtan Gilbert2018-02-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Otherwise it is possible to detect errors that are not fixed by git rebase since that works per-commit.
| | | | | | * | | | | | | | | | New IR in VM: Clambda.Gravatar Maxime Dénès2018-02-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This intermediate representation serves two purposes: 1- It is a preliminary step for primitive machine integers, as iterators will be compiled to Clambda. 2- It makes the VM compilation passes closer to the ones of native_compute. Once we unifiy the representation of values, we should be able to factorize the lambda-code generation between the two compilers, as well as the reification code. This code was written by Benjamin Grégoire and myself.
| | | | | | * | | | | | | | | | Fix map iterator on nativelambda.Gravatar Maxime Dénès2018-02-23
| | | | | | | |_|_|_|_|/ / / / | | | | | | |/| | | | | | | |
| | | | | | | | | | * | | | | Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).Gravatar Hugo Herbelin2018-02-23
| |_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | More precisely when matching "f t" with "(fun ?x => .. ((fun ?x' => ?y) ?z') ..) ?z" do not allow expansion of f since otherwise, we recursively have to match "f t" with the same pattern.
| | | | | * | | | | | | | | Document Arguments extra scopes flagGravatar Jasper Hugunin2018-02-22
| |_|_|_|/ / / / / / / / / |/| | | | | | | | | | | |
| | | | | | | | * | | | | Tweak developer documentation.Gravatar Jim Fehrle2018-02-22
| | | | | | | | | | | | |
| | | | | | | | * | | | | Rename release_lexer_state to the more descriptive get_lexer_state.Gravatar Jim Fehrle2018-02-22
| | | | | | |_|/ / / / / | | | | | |/| | | | | |
| * | | | / | | | | | | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
|/ / / / / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
| | | | | | * / / / / Remove from CircleCI builds that are already taken care of by Travis.Gravatar Théo Zimmermann2018-02-21
| |_|_|_|_|/ / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_predGravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6767: [ci] add elpiGravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6283: A pre-commit hook to magically fix whitespace issues.Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 10:17:09 +0000