aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)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
Fixes #7243.
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
This avoids having multiple highly similar things in scope when we only want one of them.
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
This makes it clear where the Not_found can come from.
2018-04-13univ minimization: comment compare_constraint_typeGaëtan Gilbert
2018-04-13niv minimization: remove [remove_lower] abbreviationGaëtan Gilbert
It's not long, used only once and it's easier to understand what it does when it's inlined.
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
ie don't go through having Eq constraints but directly to the unionfind.
2018-04-13universe minimization: cleanup using standard combinators, open UnivGaëtan Gilbert
eg Constraint.partition + filter instead of a complicated fold.
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr.
2018-04-13Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output ↵Pierre-Marie Pédrot
contains evars
2018-04-13[ltac] Deprecate nameless fix/cofix.Emilio Jesus Gallego Arias
LTAC's `fix` and `cofix` do require access to the proof object inside the tactic monad when used without a name. This is a bit inconvenient as we aim to make the handling of the proof object purely functional. Alternatives have been discussed in #7196, and it seems that deprecating the nameless forms may have the best cost/benefit ratio, so opening this PR for discussion. See also #6171.
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
We take into account all future ipats, not just the ones in the current branch
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 ↵Jason Gross
removing the test.
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
The "Stream.Error" printer does add a period, so, the messages themselves should not.
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
anymore
2018-04-12Merge PR #7107: Fixes #7100: lost of main file location in case of Ltac ↵Pierre-Marie Pédrot
failure in other file
2018-04-12[Sphinx] Add chapter 29Maxime Dénès
Thanks to Clément Pit Claudel for porting this chapter. Backport universe polymorphism changes from 2017 and 2018.
2018-04-12Attempt to fix the doubly encapsulated Ltac errors in coqide.Hugo Herbelin
It seems that ExplainErr.process_vernac_interp_error is called twice in CoqIDE. First time in Stm.stm_vernac_interp (via Stm.call_process_error_once). Second time in the "handle_exn" method used by CoqIDE to handle exceptions coming from Coq (ide_slave.ml/xmlprotocol.ml). The proposed fix is to remove the call in CoqIDE, assuming that the process_vernac_interp_error call is done otherwise on all potential error paths.
2018-04-11[sphinx] Remove migration artefacts.Théo Zimmermann
These were used very inconsistenty, serve no purpose and the link to the source is particularly useless because it's a moving target.
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
Mostly using the good option macros.
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-04-17 07:24:32 +0000