aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* configure: make Prefs a record rather than a module of refsGravatar Enrico Tassi2018-03-05
* Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Maxime Dénès2018-03-04
|\
* \ Merge PR #6876: Unify Const_sorts and Const_type, and remove VsortGravatar Maxime Dénès2018-03-04
|\ \
* \ \ Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret...Gravatar Maxime Dénès2018-03-04
|\ \ \
* \ \ \ Merge PR #6885: [stm] Partial fix for bug #6884 [location missing from replay...Gravatar Maxime Dénès2018-03-04
|\ \ \ \
* \ \ \ \ Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872]Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6882: Harden gitattributes against core.whitespace configuration.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ...Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6676: [proofview] goals come with a stateGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #915: Fix rewrite in * side conditionsGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document sup...Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | * | [VM] Unify Const_sorts and Const_type, and remove Vsort.Gravatar Maxime Dénès2018-03-02
| |_|_|_|_|_|_|_|/ / |/| | | | | | | | |
| | | | | | | * | | [stm] Partial fix for bug #6884 [location missing from replay nodes]Gravatar Emilio Jesus Gallego Arias2018-03-02
| | | | | * | | | | Harden gitattributes against core.whitespace configuration.Gravatar Gaëtan Gilbert2018-03-01
| |_|_|_|/ / / / / |/| | | | | | | |
| | | | * | | | | Fix #6878: univ undefined for [with Definition] bad instance size.Gravatar Gaëtan Gilbert2018-03-01
| |_|_|/ / / / / |/| | | | | | |
| | * | | | | | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
| | | |_|/ / / | | |/| | | |
| | | | | * | Moving code for "simple induction"/"simple destruct" to coretactics.ml4.Gravatar Hugo Herbelin2018-03-01
* | | | | | | 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
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | [toplevel] Update state when `Drop` exception is thrown [#6872]Gravatar Emilio Jesus Gallego Arias2018-02-28
| | | | | | | |/ / / | | | | | | |/| | |
| | | | | * | | | | [test-suite] Add a basic test-case for `Load`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| | | | | * | | | | [toplevel] [vernac] Remove Load hack and check supported scenarios.Gravatar Emilio Jesus Gallego Arias2018-02-28
| | | | | |/ / / /
| | | | | | | | * [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| | | | | | |_|/ | | | | | |/| |
| | | | * | | | 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
|\ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 10:36:53 +0000