aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-11-18[micromega] Sort constraints before performing `subst`BESSON Frederic
This will be more predictable. In case there are several possible substitution, the "simplest" is prefered.
2020-11-18[micromega] Simplex uses alternatively Gomory cuts and case splitsBESSON Frederic
2020-11-18[micromega] More pre-procesingBESSON Frederic
- Remove obviously redundant constraints - Perform (partial) Fourier elimination to detect (easy) cutting-planes Closes #13227
2020-11-18[micromega] Optimised cnf in case an hypothesis is trivially False.BESSON Frederic
This optimisation reduces (sometimes) the dependencies of a proof.
2020-11-18[micromega/zify] expose more API for plugin usersFrédéric Besson
2020-11-17Merge PR #13390: Intern application arguments in left-to-right ordercoqbot-app[bot]
Reviewed-by: herbelin
2020-11-17Merge PR #13397: Adding heterogeneous map on named contexts.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-17Merge PR #13404: Persistent_cache.t is always OpenPierre-Marie Pédrot
Reviewed-by: fajb
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
Reviewed-by: mattam82 Reviewed-by: maximedenes Reviewed-by: jfehrle Ack-by: gares Ack-by: Zimmi48 Ack-by: ppedrot
2020-11-17Merge PR #13402: [ci] Use lite target for Perennialcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-17[ci] Use lite target for PerennialTej Chajed
2020-11-17Persistent_cache.t is always OpenGaëtan Gilbert
2020-11-16Merge PR #12873: Unification: A type-checking fix in imitation + an error ↵coqbot-app[bot]
locating fix Reviewed-by: gares
2020-11-16Adding heterogeneous map on named contexts.Hugo Herbelin
2020-11-16Improve bad variance error message: mention expected and actual variancesGaëtan Gilbert
2020-11-16Merge PR #13040: [gc] Set GC policy as best-fit in OCaml >= 4.10.0coqbot-app[bot]
Reviewed-by: gares Reviewed-by: ppedrot
2020-11-16Merge PR #13384: Warn on hints without an explicit localitycoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-16Merge PR #13212: Suggesting to use injection when an injection pattern is ↵coqbot-app[bot]
given to destruct (wish #13205) Reviewed-by: gares Ack-by: Blaisorblade Ack-by: RalfJung
2020-11-16Merge PR #13380: Fixing the "IllTypedInstance" anomaly part of #5512coqbot-app[bot]
Reviewed-by: gares
2020-11-16Suggesting to use injection when an injection pattern is given to destruct.Hugo Herbelin
This hopefully clarifies the confusing role of destruct (see #13205).
2020-11-16[gc] Set GC policy as best-fit in OCaml >= 4.10.0Emilio Jesus Gallego Arias
Closes #11277 ; the `space_overhead` parameter has been selected for maximum speedup, in some cases it could also increase memory consumption. Please use `OCAMLRUNPARAM` to tune it and report back your experiments.
2020-11-16Merge PR #12690: Mini-fix of Locate for recursive notations using named ↵coqbot-app[bot]
variables. Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: SkySkimmer
2020-11-16Merge PR #13337: Avoid exposing an internal name when "intros _ H" fails ↵coqbot-app[bot]
because of _ being dependent in H Reviewed-by: gares
2020-11-16Add changelog for #13337.Hugo Herbelin
2020-11-16Avoid exposing an internal names when "intros _ H" fails.Hugo Herbelin
2020-11-16Merge PR #13373: Fixes #13363: in pose_all_metas_as_evars, use the context ↵coqbot-app[bot]
of the definition of the metas Reviewed-by: mattam82
2020-11-16Merge PR #12516: Deprecate `Grab Existential Variables` and `Existential` ↵Pierre-Marie Pédrot
commands Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-11-16Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"coqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-16Merge PR #13387: Fixes #12348: de Bruijn indices bug in the imitation part ↵coqbot-app[bot]
of unification Reviewed-by: mattam82
2020-11-16Merge PR #13188: Default disable automatic generalization of Instance typePierre-Marie Pédrot
Ack-by: Blaisorblade Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle Reviewed-by: ppedrot
2020-11-16Merge PR #12685: Propagating scope information in indirect application to a ↵Pierre-Marie Pédrot
reference. Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-11-16Document the deprecation of the commands.Pierre-Marie Pédrot
2020-11-16Document the new warning.Pierre-Marie Pédrot
2020-11-16Tentative fix for the refman.Pierre-Marie Pédrot
2020-11-16Fix test-suite.Pierre-Marie Pédrot
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
By default Coq stdlib warnings raise an error, so this is really required.
2020-11-16Warning on hint commands that have no explicit locality.Pierre-Marie Pédrot
2020-11-16Merge PR #13388: Export locality for all hint commandscoqbot-app[bot]
Reviewed-by: silene Reviewed-by: gares Reviewed-by: Zimmi48
2020-11-16Deprecate `Grab Existential Variables` and `Existential` commandsMaxime Dénès
2020-11-16Overlay for Coq-Equations.Hugo Herbelin
2020-11-16Checking type in unification imitation: avoid raising a non-located error.Hugo Herbelin
2020-11-16Fixing a (known) "bugged" part of imitation in unification.Hugo Herbelin
We ensure that when imitation stops to be possible, we postpone an equation of the type of the subterm (and not of the arbitrary type of an evar possibly depending on this subterm).
2020-11-16Merge PR #13365: Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-freecoqbot-app[bot]
Reviewed-by: anton-trunov Reviewed-by: Blaisorblade
2020-11-16Fixing the "IllTypedInstance" anomaly part of #5512.Hugo Herbelin
It remains to accept resolving Type(u)<=Prop for u arbitrary sort variable.
2020-11-16Update grammar in docJim Fehrle
2020-11-16Changelog for variance syntaxGaëtan Gilbert
2020-11-16Overlays for cumulative inductive syntaxGaëtan Gilbert
2020-11-16Doc for variance syntaxGaëtan Gilbert
2020-11-16Syntax for specifying cumulative inductivesGaëtan Gilbert
2020-11-16Infrastructure for cumulative inductive syntax (no grammar extension yet)Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:43:45 +0000