aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-03-05Sanitize universe declaration in Context (stop using a ref...)Gaëtan Gilbert
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-04Merge PR #6736: [toplevel] Move beautify to its own pass.Maxime Dénès
2018-03-04Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Maxime Dénès
2018-03-04Merge PR #6876: Unify Const_sorts and Const_type, and remove VsortMaxime Dénès
2018-03-04Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret...Maxime Dénès
2018-03-04Merge PR #6885: [stm] Partial fix for bug #6884 [location missing from replay...Maxime Dénès
2018-03-04Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872]Maxime Dénès
2018-03-04Merge PR #6882: Harden gitattributes against core.whitespace configuration.Maxime Dénès
2018-03-04Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ...Maxime Dénès
2018-03-04Merge PR #6676: [proofview] goals come with a stateMaxime Dénès
2018-03-04Merge PR #915: Fix rewrite in * side conditionsMaxime Dénès
2018-03-04Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document sup...Maxime Dénès
2018-03-02CHANGES entry for #6791.Théo Zimmermann
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
2018-03-02Turn warning for deprecated notations on.Théo Zimmermann
2018-03-02Remove the deprecation for some 8.2-8.5 compatibility aliases.Théo Zimmermann
2018-03-02[VM] Unify Const_sorts and Const_type, and remove Vsort.Maxime Dénès
2018-03-02[stm] Partial fix for bug #6884 [location missing from replay nodes]Emilio Jesus Gallego Arias
2018-03-01Harden gitattributes against core.whitespace configuration.Gaëtan Gilbert
2018-03-01Fix #6878: univ undefined for [with Definition] bad instance size.Gaëtan Gilbert
2018-03-01Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Hugo Herbelin
2018-03-01Moving code for "simple induction"/"simple destruct" to coretactics.ml4.Hugo Herbelin
2018-03-01Merge PR #6856: travis: elpi needs findlib >= 1.5Maxime Dénès
2018-03-01Merge PR #6864: Remove empty, wrongly located, doc file.Maxime Dénès
2018-03-01Merge PR #6861: Typo in the documentation of the `pattern` tacticMaxime Dénès
2018-03-01Merge PR #6850: Fix #6751 trust_file_cache logic was invertedMaxime Dénès
2018-02-28[toplevel] Update state when `Drop` exception is thrown [#6872]Emilio Jesus Gallego Arias
2018-02-28[toplevel] Move beautify to its own pass.Emilio Jesus Gallego Arias
2018-02-28[test-suite] Add a basic test-case for `Load`.Emilio Jesus Gallego Arias
2018-02-28[toplevel] [vernac] Remove Load hack and check supported scenarios.Emilio Jesus Gallego Arias
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-28travis: elpi needs findlib >= 1.5Enrico Tassi
2018-02-28tavis: make the . in pkg.version part of $VERSIONEnrico Tassi
2018-02-28Merge PR #6847: Fix make source-docMaxime Dénès
2018-02-28Merge PR #6854: comment "resolvability" bit in Evd.evar_mapMaxime Dénès
2018-02-28Merge PR #6852: [stdlib] move “Require” out of sectionsMaxime Dénès
2018-02-28Merge PR #6853: Add a comment on EConstr.to_constr regarding evar-freeness.Maxime Dénès
2018-02-28Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmasMaxime Dénès
2018-02-28Merge PR #6756: Fix issue with spurious timing test failuresMaxime Dénès
2018-02-28Merge PR #6788: Fixes #6787 (minus sign interpreted by coqdoc as a bullet in ...Maxime Dénès
2018-02-28Merge PR #6789: Check whitespace errors per-commit.Maxime Dénès
2018-02-28Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Maxime Dénès
2018-02-28Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit...Maxime Dénès
2018-02-28Merge PR #6812: Rename release_lexer_state to the more descriptive get_lexer_...Maxime Dénès
2018-02-28Merge PR #6752: Remove from CircleCI builds that are already taken care of by...Maxime Dénès
2018-02-28Remove empty, wrongly located, doc file.Théo Zimmermann
2018-02-27Typo in the documentation of the `pattern` tacticJoachim Breitner
2018-02-27comment "resolvability" bit in Evd.evar_mapEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 07:32:09 +0000