aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2020-11-25Merge PR #13447: Remove unused parsing codecoqbot-app[bot]
Reviewed-by: herbelin
2020-11-25Merge PR #13228: [micromega] Performance of liaPierre-Marie Pédrot
Reviewed-by: ppedrot Ack-by: vbgl
2020-11-25Merge PR #13405: Alternative implementation of the Micromega persistent cacheVincent Laporte
Reviewed-by: vbgl
2020-11-24Keep accessed objects in memory in Persistent_cache.Pierre-Marie Pédrot
2020-11-24Alternative implementation of the Micromega persistent cache.Pierre-Marie Pédrot
Instead of loading the whole file in memory, we simply load an index table associating a file position to a key hash. Cache access is then performed on the fly by unmarshalling the data whose hash corresponds and checking key equality.
2020-11-24Preserve sharing in the Micromega cache.Pierre-Marie Pédrot
For some reason it was explicitly deactivated since the file was added, but I have no idea why. Unsetting sharing would lead to potential explosive memory consumption at unmarshalling time which is not worth the minimal cost it has at marshalling time.
2020-11-24Add an explicit signature to the MakeCache functor in Micromega.Pierre-Marie Pédrot
2020-11-23Fix comparison of extracted array literalsGaëtan Gilbert
Fixes #13453 which was a loop in ~~~ocaml let normalize a = let o = optims () in let rec norm a = let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in if eq_ml_ast a a' then a else norm a' in norm a ~~~ the `eq_ml_ast` was always returning `false`.
2020-11-23Merge PR #13417: Use nat_or_var in grammar where negative values don't make ↵coqbot-app[bot]
sense Reviewed-by: Zimmi48
2020-11-22Remove unused parsing codeJim Fehrle
2020-11-21Merge PR #12246: Adding support for applying in several hypotheses at the ↵Pierre-Marie Pédrot
same time (granting #9816) Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-11-20A step towards supporting pattern cast deeplier.Hugo Herbelin
We at least support a cast at the top of patterns in notations.
2020-11-20Add preliminary support for notations with large class (non-recursive) binders.Hugo Herbelin
We introduce a class of open binders which includes "x", "x:t", "'pat" and a class of closed binders which includes "x", "(x:t)", "'pat".
2020-11-20Merge PR #13399: Miscellaneous ring improvements in code + error messagesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-20Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clausesPierre-Marie Pédrot
Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-20Granting #9816: apply in takes several hypotheses.Hugo Herbelin
2020-11-20Merge PR #13403: Use only nats for occs_nums rather than intscoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: herbelin
2020-11-19Use a proper canonical structure entry for projections.Hugo Herbelin
This is to make more explicit that arguments of the projection are not kept. We seize this opportunity to use QGlobRef equality on GlobRef.
2020-11-18Use only nats for occs_nums rather than intsJim Fehrle
2020-11-18Merge PR #13341: Finish fixing setoid rewrite under anonymous lambdas ↵Pierre-Marie Pédrot
(hopefully) Reviewed-by: ppedrot
2020-11-18Merge PR #13251: Make sure that setoid_rewrite passes state to subgoalsPierre-Marie Pédrot
Reviewed-by: ppedrot
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 #13404: Persistent_cache.t is always OpenPierre-Marie Pédrot
Reviewed-by: fajb
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-16Other renamings evd -> sigma in newring.ml.Hugo Herbelin
2020-11-16Pass sigma functionally in newring.ml.Hugo Herbelin
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-16Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"coqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-16Finish fixing setoid rewrite under anonymous lambdas (hopefully)Gaëtan Gilbert
Fix #13246 Not sure if this is the right thing to do, but it seems to work.
2020-11-15Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"Jim Fehrle
2020-11-15Implement export locality for the remaining Hint commands.Pierre-Marie Pédrot
2020-11-15Merge PR #13339: In -noinit mode, add support for Proof using, using is not ↵Pierre-Marie Pédrot
a keyword. Ack-by: SkySkimmer Reviewed-by: herbelin Ack-by: ppedrot
2020-11-12Merge PR #13253: Change Dumpglob.pause and Dumpglob.continue into push and popcoqbot-app[bot]
Reviewed-by: gares Ack-by: SkySkimmer Ack-by: ejgallego
2020-11-12Change Dumpglob.pause and Dumpglob.continue into push and popLasse Blaauwbroek
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-11-12Revert to "using" not being a keyword in -noinit mode.Théo Zimmermann
The IDENT annotations in g_ltac.mlg are required to not break the parser.
2020-11-12Add support for Proof using in -noinit mode.Théo Zimmermann
"Proof with" is Ltac-specific but there is no reason why it should be the same for "Proof using".
2020-11-10Convert logic.rst to prodnJim Fehrle
2020-11-06Merge PR #13284: Fixing interpretation of rewrite_strat argument in LtacPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
Reviewed-by: herbelin Reviewed-by: JasonGross Reviewed-by: jfehrle Ack-by: Zimmi48
2020-11-05[string notation] Handle parameterized inductives and non inductivesPierre Roux
2020-11-05Merge numeral and string notation pluginsPierre Roux
2020-11-05[numeral notation] Add support for parameterized inductivesPierre Roux
2020-11-05[numeral notation] Handle implicit argumentsPierre Roux
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 04:53:31 +0000