aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
We do two changes: - We distinguish between a notion of format generically attached to notations and a new notion of format attached to interpreted notations. "Reserved Notation" attaches a format generically. "Notation" attaches the format specifically to the given interpretation, and additionally, attaches it generically if it is the first time the notation is defined. - We warn before overriding an explicitly reserved generic format, or a specific format.
2020-02-18Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.Théo Zimmermann
Reviewed-by: Zimmi48
2020-02-14Use thunks to univ instead of lazy constr for template typingGaëtan Gilbert
2020-02-14Merge PR #11584: Add #[uniform] and #[nonuniform] (for Uniform Inductive ↵Maxime Dénès
Parameters) Reviewed-by: Matafou Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
Currently, `.v` under the `Coq.` prefix are found in both `theories` and `plugins`. Usually these two directories are merged by special loadpath code that allows double-binding of the prefix. This adds some complexity to the build and loadpath system; and in particular, it prevents from handling the `Coq.*` prefix in the simple, `-R theories Coq` standard way. We thus move all `.v` files to theories, leaving `plugins` as an OCaml-only directory, and modify accordingly the loadpath / build infrastructure. Note that in general `plugins/foo/Foo.v` was not self-contained, in the sense that it depended on files in `theories` and files in `theories` depended on it; moreover, Coq saw all these files as belonging to the same namespace so it didn't really care where they lived. This could also imply a performance gain as we now effectively traverse less directories when locating a library. See also discussion in #10003
2020-02-13Merge PR #11417: Move kind_of_type from the kernel to EConstr.Enrico Tassi
Reviewed-by: SkySkimmer Reviewed-by: gares
2020-02-13Don't duplicate the inductive keyword for each block elt when parsingGaëtan Gilbert
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-21 09:27:48 +0000