aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2020-02-06unsafe_type_of -> type_of in Rewrite.build_morphism_signatureGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Rewrite.resolve_morphismGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Rewrite.decompose_app_relGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Firstorded.Instances.mk_open_instanceGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Sequent.extend_with_auto_hintsGaëtan Gilbert
+ fix evar leak in caller
2020-02-03Fix efficiency regression #11436Frédéric Besson
- The cutting plane has been (sometimes) improved to generate stronger cuts. - There is now some support for profiling the Simplex see documentation for Show Lia Profile.
2020-01-30Do not rely on Libobject for the current environment in extraction.Pierre-Marie Pédrot
Instead, we export in Safe_typing the current module declaration.
2020-01-30Merge PR #11307: Remove the hacks relying on hardwired libobject tags.Maxime Dénès
Reviewed-by: maximedenes
2020-01-28Fix #11467Pierre Roux
'e' was not displayed when printing decimal notations in R : Require Import Reals. Check (1.23e1, 32e+1, 0.1)%R. was giving < (123-1%R, 321%R, 1-1%R) instead of < (123e-1%R, 32e1%R, 1e-1%R) This was introduced in #8764 (in Coq 8.10).
2020-01-17Merge PR #11362: Lia bugfix 11191Maxime Dénès
Reviewed-by: maximedenes
2020-01-14[zify] elim let in MLFrédéric Besson
2020-01-08Factorize ascii extraction in ExtrOcamlChar.vMaxime Dénès
2020-01-08Better extraction of string literals in HaskellMaxime Dénès
2020-01-08Reimplement string <-> char list conversionsXavier Leroy
Using only OCaml stdlib functions available in OCaml 4.05.
2020-01-08Typo in commentXavier Leroy
2020-01-08Rename ExtrOcamlStringPlus into ExtrOcamlNativeStringXavier Leroy
As suggested during review. That's a much better name.
2020-01-08Avoid hardcoded paths in extractionMaxime Dénès
2020-01-08Avoid warning 40Maxime Dénès
2020-01-08Support extraction of Coq's string type to OCaml's string type, continuedXavier Leroy
Address issues found in CI testing and in code review.
2020-01-08Support extraction of Coq's string type to OCaml's string typeXavier Leroy
Instead of the default extraction to OCaml's "char list" type.
2020-01-06[micromega] fix of bug #11191Frédéric Besson
- Add an instance to ZifyInst to instruct zify that 0 < x -> 0 < y -> 0 < Z.pow x y - More aggressive interval analysis to bound non-linear monomials.
2020-01-03Merge PR #11343: fix: Shorten ssrsetoid.v to fix TC performance issueEnrico Tassi
Reviewed-by: gares
2019-12-31Merge PR #11338: Remove uses of Global in Evd API.Gaëtan Gilbert
Reviewed-by: ejgallego Reviewed-by: herbelin
2019-12-27fix: Shorten ssrsetoid.vErik Martin-Dorel
* This patch is a quick fix that removes part of the features of coq/coq#10022, namely the ability to directly use setoid_rewrite with a (Under_rel)-tagged relation R. This just means we'll need to do an extra step [rewrite UnderE.] which was unnecessary with Coq 8.11+alpha. * This PR stays backward-compatible w.r.t. Coq 8.10 and also keeps the salient feature of coq/coq#10022 (generalize under & over to any Reflexive relation). * Related: coq-community/atbr#23
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional environment instead of querying the imperative global one. We percolate this change as higher up as possible.
2019-12-26[omega] Remove non-documented "omega with *"Emilio Jesus Gallego Arias
This form is only used in coq-bignums and not documented. I think removal is the best choice, specially as `zify` is not part of the omega plugin anymore.
2019-12-26Deprecate the "omega with *" syntax.Pierre-Marie Pédrot
Changes to the test-suite were backported from PR #11288.
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
We restrict to those that are actually related to typeclasses, and perform the following renamings: Classops --> Coercionops Class --> ComCoercion
2019-12-22Remove the hacks relying on hardwired libobject tags.Pierre-Marie Pédrot
The patch is done in a minimal way. The hacks are turned into a new kind of safer hacks, but hacks nonetheless. They should go away at some point, but the current patch is focussed on the removal of Libobject cruft, not making the dirty code of its upper-layer callers any cleaner.
2019-12-18Merge PR #11027: Cleanup post #10647 (expose comind universe handling)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-12-18Merge PR #11203: Make the string argument of `time` print correctlyPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
PR #9725 fixes completness bugs introduces some inefficiency. The current PR intends to fix the inefficiency while retaining completness. The fix removes a pre-processing step and instead relies on a more elaborate proof format introducing positivity constraints on the fly. Solve bootstrapping issues: RMicromega <-> Rbase <-> lia. Fixes #11063 and fixes #11242 and fixes #11270
2019-12-16Pretyping.check_evars: make initial evar map optionalGaëtan Gilbert
There are no users in Coq but maybe some plugin wants it so don't completely remove it
2019-12-13[micromega] Enable ocamlformat.Emilio Jesus Gallego Arias
2019-12-11Remove the reliance of ring objects on the named part.Pierre-Marie Pédrot
This was just dead code.
2019-12-10Side-effect free wrapper around already declared schemes.Pierre-Marie Pédrot
Some calls are actually guarded by a check that the scheme is already in the cache. There is no reason to generate dummy side-effects in that case.
2019-12-06Make the string argument of `time` print correctlyJason Gross
Fixes #10971
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
This allows to give access to all printing options (e.g. a scope or being-in-context) to every printer w/o increasing the numbers of functions.
2019-12-05Merge PR #11241: Unfortunate Coq 8.10 bug with "cofix with" tactic syntaxEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-12-05Unfortunate bug with "cofix with": case of a CProdN over no bindings.Hugo Herbelin
Failing on CProdN([],...) was maybe a bit too radical.
2019-12-05Merge PR #11210: Tacinterp: push_trace doesn't need to be wrapped in a tacticPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
The manual was already saying that it was deprecated, but no warning was emitted. Fixes #10572
2019-11-29Merge PR #11184: Undeprecate Add Setoid / Add Morphism.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-29Merge PR #11076: Remove all remaining calls to “omega” from the standard ↵Emilio Jesus Gallego Arias
library Reviewed-by: ejgallego
2019-11-29Merge PR #11186: Remove undocumented and deprecated `Congruence Depth` optionPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-28Tacinterp: push_trace doesn't need to be wrapped in a tacticGaëtan Gilbert
This lets us get rid of dummy proofview manips. Simplifications based on [(tclUNIT foo >>= f) = f foo]
2019-11-26Remove undocumented and deprecated `Congruence Depth` optionMaxime Dénès
It was a no-op.
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
Using the parameter universes in the constructor causes implicit equality constraints, so those universes may not be template polymorphic. A couple types in the stdlib were erroneously marked template, which is now detected. Removing the marking doesn't actually change behaviour though. Also fixes #10504.
2019-11-26Undeprecate Add Setoid / Add Morphism.Théo Zimmermann
The proposed replacements are not satisfying because they are more complicated to use. Following the discussion in #8713, we decide to remove the deprecation warning for these commands.
2019-11-25Nsatz: use “lia” rather than “omega”Vincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 12:58:19 +0000