aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-03-13Allow scope delimiters in Ltac2 open_constr:(...) quotation.Pierre-Marie Pédrot
Fixes #12806: Ltac2 Notation's open_constr should accept scope stacks.
2021-03-12Merge PR #13907: Algorithmically faster algorithm for term replacing.coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-03-12Further simplification of the term replacing code.Pierre-Marie Pédrot
We factorize the code for replace and subst, since it seems there is no reason to keep them separate, not even performance. Some static invariants are made explicit in the API.
2021-03-12Algorithmically faster algorithm for term replacing.Pierre-Marie Pédrot
Instead of recomputing the n-th lifts of terms for every subterm under a context, we introduce a table storing the value of this lift across contexts. While not the most efficient algorithmically, it is still much more efficient in practice and does not exhibit the exponential behaviour of replacing under different subcontexts. In an ideal world we would have an equality function on terms that allows to compute equality up to lifts, which would prevent having to even compute the lift at all, but the current fix has the advantage to be self-contained and not require dangerous tweaking of an equality function which is already complex enough as it is. Fixes #13896: cbn very slow.
2021-03-11Merge PR #13854: Normalize evars during bytecode compilation.coqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: ppedrot Ack-by: ejgallego
2021-03-10Merge PR #13922: Mention overlays in PR templatecoqbot-app[bot]
Reviewed-by: Zimmi48
2021-03-10Mention overlays in PR templateGaëtan Gilbert
2021-03-10Merge PR #13901: Fix list contributorscoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-03-10Merge PR #13840: [notation] option to fine tune printing of literalscoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: jfehrle
2021-03-10Merge PR #13912: Refactor coercionopscoqbot-app[bot]
Reviewed-by: gares
2021-03-10Merge PR #13919: Fix a hyperlink in CONTRIBUTING.mdcoqbot-app[bot]
Reviewed-by: Zimmi48
2021-03-10Fix a hyperlink in CONTRIBUTING.mdKazuhiko Sakaguchi
2021-03-09Add changelogKazuhiko Sakaguchi
2021-03-09Add overlayKazuhiko Sakaguchi
2021-03-09Add the source and target classes to the coercion tableKazuhiko Sakaguchi
`coe_source` and `coe_target` fields of type `cl_typ` have been added to `coe_info_typ` so that it allows querying the classes from a `GlobRef.t` of a coercion. The `coercion` record has also been replaced with `coe_info_typ`.
2021-03-09Replace cl_index with cl_typ in coercionops.mlKazuhiko Sakaguchi
The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been replaced with `cl_typ` and `ClTypMap` respectively.
2021-03-08Merge PR #13707: Convert 2nd part of rewriting chapter to prodncoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-03-07Merge PR #13910: Attempt to fix the bench after coq-core splitPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-07Attempt to fix the bench after coq-core splitGaëtan Gilbert
2021-03-06Merge PR #13586: Support nested timeoutsPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-06Merge PR #13882: Fix #12011 ssreflect "rewrite in" with setoidsPierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2021-03-06Merge PR #13236: Add a type of format strings to Ltac2.Michael Soegtrop
Reviewed-by: JasonGross Reviewed-by: MSoegtropIMC
2021-03-06Merge PR #13902: [coercion] expose coercion_infoPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-06Merge PR #13899: Add noncritical constraint to exception catching in ↵Pierre-Marie Pédrot
solve_constraints Reviewed-by: ppedrot
2021-03-05Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12)Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2021-03-05[coercipn] expose coercion_infoEnrico Tassi
2021-03-05Update nixpkgs.Théo Zimmermann
To get the right version of git to use the list-contributors.sh script.
2021-03-05Fix the .mailmap.Théo Zimmermann
2021-03-05Document the relation of the list-contributors.sh script to .mailmap.Théo Zimmermann
2021-03-05Fix list-constributors.sh script.Théo Zimmermann
2021-03-05Merge PR #13900: doc: don't count a contributor twice in the changelogcoqbot-app[bot]
Reviewed-by: Zimmi48
2021-03-04Correctly sort the glossaryJim Fehrle
2021-03-04doc: don't count a contributor twice in the changelogLi-yao Xia
2021-03-04Merge PR #13897: Cleanup internal hint locality handlingcoqbot-app[bot]
Reviewed-by: ppedrot Reviewed-by: ejgallego
2021-03-04Add noncritical constraint to exception catching in solve_constraintsLasse Blaauwbroek
2021-03-04Properly support nested timeoutsLasse Blaauwbroek
2021-03-04Cleanup internal hint locality handlingGaëtan Gilbert
By separating the libobject for create db and other hints we can unify handling of local/superglobal.
2021-03-04[test-suite] test for primitive tokens in patternsEnrico Tassi
2021-03-04[doc] changelog entryEnrico Tassi
2021-03-04[doc] Set/Unset Printing Raw LiteralsEnrico Tassi
2021-03-04[notation] option to fine tune printing of literalsEnrico Tassi
2021-03-04Fix #12011 ssreflect "rewrite in" with setoidsGaëtan Gilbert
ssreflect asks setoid rewrite to rewrite in goal "forall_special_name_ : T, _other_name_" Since this is a non dependent product, setoid rewrite converts that to "impl T _other_name_" and must be taught to restore the special name when unfolding impl.
2021-03-03Merge PR #12567: [build] Split stdlib to it's own package.coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross Ack-by: gares Ack-by: LasseBlaauwbroek Ack-by: silene Ack-by: vbgl
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
We introduce a new package structure for Coq: - `coq-core`: Coq's OCaml tools code and plugins - `coq-stdlib`: Coq's stdlib [.vo files] - `coq`: meta-package that pulls `coq-{core,stdlib}` This has several advantages, in particular it allows to install Coq without the stdlib which is useful in several scenarios, it also open the door towards a versioning of the stdlib at the package level. The main user-visible change is that Coq's ML development files now live in `$lib/coq-core`, for compatibility in the regular build we install a symlink and support both setups for a while. Note that plugin developers and even `coq_makefile` should actually rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust. There is a transient state where we actually look for both `$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support the non-ocamlfind plus custom variables. This will be much improved once #13617 is merged (which requires this PR first), then, we will introduce a `coq.boot` library so finally `coqdep`, `coqchk`, etc... can share the same path setup code. IMHO the plan should work fine.
2021-03-02Merge PR #13889: Dead code elimination: not reducible error message is never ↵coqbot-app[bot]
raised. Reviewed-by: jfehrle
2021-03-02Merge PR #13891: Simplify installation instructions in README.coqbot-app[bot]
Reviewed-by: jfehrle
2021-03-02Simplify wording.Théo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2021-03-02Simplify installation instructions in README.Théo Zimmermann
Now that they are well described on the website.
2021-03-02Dead code elimination: not reducible error message is never raised.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 04:20:41 +0000