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-17Adding change log for #12984.Hugo Herbelin
Co-authored-by: Ralf Jung <post@ralfj.de>
2020-11-17Documenting priority given to most recently declared/imported notations.Hugo Herbelin
2020-11-17A reimport of notations now put the corresponding notations again in front.Hugo Herbelin
2020-11-17Add changelog for #12986.Hugo Herbelin
2020-11-17Documenting the preference given to more precise notations at printing time.Hugo Herbelin
2020-11-17For printing, ordering notations by precision of the pattern.Hugo Herbelin
This relies on finer-than partial order check with. In particular: - number and order of notation metavariables does not matter - take care of recursive patterns inclusion
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-17Fixes #13235: remove fragile tolerance for degenerate in-hyps clause.Hugo Herbelin
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-11-16Improve some error messages.Vincent Semeria
This also includes aligning with refman when relevant and using capital letters and final period.
2020-11-16Adding Array.iter3.Hugo Herbelin
2020-11-16Fixing alpha-equality of notation interpretations with recursive patterns.Hugo Herbelin
The name bound in binders were not checked up to alpha-equivalence, nor were the names binding the recursive patterns.
2020-11-16[doc] add a link to v8.13Enrico Tassi
2020-11-16Other renamings evd -> sigma in newring.ml.Hugo Herbelin
2020-11-16Pass sigma functionally in newring.ml.Hugo Herbelin
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-16Using labels to document match_notation_constr.Hugo Herbelin
2020-11-16Add change log for #12965.Hugo Herbelin
2020-11-16Fix #9569 (notations collect the spine binding variables at printing time).Hugo Herbelin
This allows to know which global references whose basename may be unexpectedly caught need to be qualified. Note: the alternative strategy, which is sometimes used, of renaming the binding variables so as to avoid collisions with the basename of a global reference is somehow less nice.
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-16Fix incorrect name refreshing when interning a generalized binderGaëtan Gilbert
Fix #13249
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 15:50:01 +0000