aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-04-14Merge PR #7136: Evar maps contain econstrs.Pierre-Marie Pédrot
2018-04-14Merge PR #7217: Sphinx doc chapter 1Théo Zimmermann
2018-04-14Add missing CHANGES entry for #6169.Théo Zimmermann
2018-04-13Making tactic-in-term aware of "Set Ltac Debug".Hugo Herbelin
2018-04-13Update the CI branch for Equations.Théo Zimmermann
2018-04-13Overlay for econstr in Evd.Gaëtan Gilbert
2018-04-13[coq_makefile] COQMF_WINDRIVE is empty on linux (fix #7233)Enrico Tassi
2018-04-13univ minimization: comment [enforce_uppers]Gaëtan Gilbert
2018-04-13univ minimization [enforce_upper]: replace Option.get with matchGaëtan Gilbert
2018-04-13univ minimization: Partially let-lift [enforce_uppers]Gaëtan Gilbert
2018-04-13univ minimization: rename acc' -> enforce_uppersGaëtan Gilbert
2018-04-13univ minimization: use shadowing moreGaëtan Gilbert
2018-04-13univ minimization: let-lift [not_lower]Gaëtan Gilbert
2018-04-13univ minimization: simplify try-with block around find_instsGaëtan Gilbert
2018-04-13univ minimization: s/[failwith ""]/[raise UpperBoundedAlg]/Gaëtan Gilbert
2018-04-13univ minimization: simplify try-with block around [find u left]Gaëtan Gilbert
2018-04-13univ minimization: comment compare_constraint_typeGaëtan Gilbert
2018-04-13niv minimization: remove [remove_lower] abbreviationGaëtan Gilbert
2018-04-13minimize_univ_variables: bool*bool*univ*lowermap replaced by recordGaëtan Gilbert
2018-04-13minimize_univ_variables: remove [and right] abbreviation.Gaëtan Gilbert
2018-04-13universe normalisation: put equivalence class partition in UGraphGaëtan Gilbert
2018-04-13universe minimization: cleanup using standard combinators, open UnivGaëtan Gilbert
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-04-13Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contain...Pierre-Marie Pédrot
2018-04-13[ltac] Deprecate nameless fix/cofix.Emilio Jesus Gallego Arias
2018-04-13[Sphinx] Add Chapter 1Maxime Dénès
2018-04-13[Sphinx] Move chapter 1 to new infrastructureMaxime Dénès
2018-04-13Merge PR #7117: Sphinx doc chapter 29Théo Zimmermann
2018-04-13[ssr] fix delayed clears (fix #7045)Enrico Tassi
2018-04-13Merge PR #7231: Fixing the 3 cases of a "Stream.Error" ended with two periods.Enrico Tassi
2018-04-12Merge PR #7222: [sphinx] Remove migration artefacts.Maxime Dénès
2018-04-12Merge PR #7194: [warnings] Remove `set_current_loc` hack.Maxime Dénès
2018-04-12Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by removin...Jason Gross
2018-04-12Merge PR #7202: Correction of ugly message described in #4667Pierre Courtieu
2018-04-12Merge PR #7220: Many Sphinx fixes (including a fix of the credits chapter)Maxime Dénès
2018-04-12Merge PR #7201: Translation fixes in chapter syntax extensions.Maxime Dénès
2018-04-12Merge PR #6972: [api] Deprecate a couple of aliases that we missed.Maxime Dénès
2018-04-12Merge PR #500: Move bugs that have been closed on BugzillaMaxime Dénès
2018-04-12Fixing the 3 cases of a "Stream.Error" ended with two periods.Hugo Herbelin
2018-04-12Merge PR #7087: Congruence tactic engine updatePierre-Marie Pédrot
2018-04-12Merge PR #7096: coqide: avoid marking sentences that are not in the document ...Pierre-Marie Pédrot
2018-04-12Merge PR #7107: Fixes #7100: lost of main file location in case of Ltac failu...Pierre-Marie Pédrot
2018-04-12[Sphinx] Add chapter 29Maxime Dénès
2018-04-12Attempt to fix the doubly encapsulated Ltac errors in coqide.Hugo Herbelin
2018-04-11[sphinx] Remove migration artefacts.Théo Zimmermann
2018-04-11[Sphinx] Move chapter 29 to new infrastructureMaxime Dénès
2018-04-11Fix the status of some resolved bugsTej Chajed
2018-04-11[sphinx] Use macros for notes and examples.Théo Zimmermann
2018-04-11[sphinx] Fixes in chapter 2.Théo Zimmermann
2018-04-11Remove empty reference to the current version of Coq.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 09:46:06 +0000