aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Pass the constant cache as a separate argument in kernel reduction.Gravatar Pierre-Marie Pédrot2018-03-04
* 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
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ 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 infinit...Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6812: Rename release_lexer_state to the more descriptive get_lexer_...Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6752: Remove from CircleCI builds that are already taken care of by...Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | * 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
| |_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | |
| | | | | | | | | * | | 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
| |_|_|_|_|_|_|_|/ |/| | | | | | | |
| | | | | | | * | [test-suite] Move sed scripts into bash arraysGravatar Jason Gross2018-02-24
* | | | | | | | | 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 serial...Gravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | * | | | Check whitespace errors per-commit.Gravatar Gaëtan Gilbert2018-02-23
| | | | | | * | | | | | | | | | New IR in VM: Clambda.Gravatar Maxime Dénès2018-02-23
| | | | | | * | | | | | | | | | 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
| |_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | |
| | | | | * | | | | | | | | 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
|/ / / / / / / / / / /
| | | | | | * / / / / 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
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just the...Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 03:43:29 +0000