aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2020-12-02Merge PR #13275: Put all Int63 primitives in a separate fileVincent Laporte
Ack-by: SkySkimmer Ack-by: ppedrot Reviewed-by: vbgl
2020-12-02Put all Int63 primitives in a separate filePierre Roux
Following a request from Pierre-Marie Pédrot in #13258
2020-12-01Fix a bug in funind.Pierre-Marie Pédrot
It was generating a completely nonsense case branch, but for some reason the proof still went trough.
2020-11-29Merge PR #13510: Add missing print registration for wit_nat_or_varcoqbot-app[bot]
Reviewed-by: herbelin
2020-11-29Fixing printing of apply in (continuation of #12246).Hugo Herbelin
2020-11-28Add missing print registration for wit_nat_or_varJim Fehrle
2020-11-27Revert "Remove deprecated tactic cutrewrite."Théo Zimmermann
This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
2020-11-26Merge PR #13415: Separate interning and pretyping of universescoqbot-app[bot]
Reviewed-by: mattam82
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-25Separate interning and pretyping of universesGaëtan Gilbert
This allows proper treatment in notations, ie fixes #13303 The "glob" representation of universes (what pretyping sees) contains only fully interpreted (kernel) universes and unbound universe ids (for non Strict Universe Declaration). This means universes need to be understood at intern time, so intern now has a new "universe binders" argument. We cannot avoid this due to the following example: ~~~coq Module Import M. Universe i. End M. Definition foo@{i} := Type@{i}. ~~~ When interning `Type@{i}` we need to know that `i` is locally bound to avoid interning it as `M.i`. Extern has a symmetrical problem: ~~~coq Module Import M. Universe i. End M. Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}. Print foo. (* must not print Type@{i} -> Type@{i} *) ~~~ (Polymorphic as otherwise the local `i` will be called `foo.i`) Therefore extern also takes a universe binders argument. Note that the current implementation actually replaces local universes with names at detype type. (Asymmetrical to pretyping which only gets names in glob terms for dynamically declared univs, although it's capable of understanding bound univs too) As such extern only really needs the domain of the universe binders (ie the set of bound universe ids), we just arbitrarily pass the whole universe binders to avoid putting `Id.Map.domain` at every entry point. Note that if we want to change so that detyping does not name locally bound univs we would need to pass the reverse universe binders (map from levels to ids, contained in the ustate ie in the evar map) to extern.
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>
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 06:16:25 +0000