aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2020-02-13Merge PR #11417: Move kind_of_type from the kernel to EConstr.Enrico Tassi
Reviewed-by: SkySkimmer Reviewed-by: gares
2020-02-13Merge PR #11521: Remove Goptions.opt_name fieldPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
The standard use is to repeat the option keywords in lowercase, which is basically useless. En passant add doc entry for Dump Arith.
2020-02-12Standardize constr -> globref operations to use destRef/isRef/isRefXGaëtan Gilbert
Instead of various termops and globnames aliases.
2020-02-11Merge PR #11235: Add syntax for non maximal implicit argumentsHugo Herbelin
Reviewed-by: herbelin Reviewed-by: jfehrle Ack-by: maximedenes
2020-02-07Remove unsafe_type_of from funindGaëtan Gilbert
2020-02-07various unsafe_type_of -> type_of_variable in funindGaëtan Gilbert
This is the easy part of removing unsafe_type_of, as type_of_variable doesn't return (or even take as argument) an evar map.
2020-02-07Remove confusing commented code in funindGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in CcalgoGaëtan Gilbert
Not sure about these, let's see how it goes.
2020-02-06unsafe_type_of -> type_of in Cctac (with small refactor)Gaëtan Gilbert
Not sure if get_type_of would be fine, let's go with this for now.
2020-02-06unsafe_type_of -> get_type_of in Coq_omega.destructure_hypsGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Extractactics.destauto_inGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Extractactics.mkCaseEqGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Rewrite.symmetry_inGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Rewrite.default_morphismGaëtan Gilbert
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-05[cleanup] remove useless EConstr qualificationsEnrico Tassi
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
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-02-02Move kind_of_type from the kernel to ssr.Pierre-Marie Pédrot
It was virtually unused except in ssr, and there is no reason to clutter the kernel with irrelevant code. Fixes #9390: What is the purpose of the function "kind_of_type"?
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 01:35:37 +0000