aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-03-16add results on to_listOlivier Laurent
2021-03-14Merge PR #13935: Fixed grammar productions for PDF documentationscoqbot-app[bot]
Reviewed-by: jfehrle
2021-03-13Merge PR #13917: Add deriving lib to CI.coqbot-app[bot]
Reviewed-by: ejgallego Ack-by: SkySkimmer
2021-03-13Merge PR #13931: noglob/dumpglob should be in coqc specific usagecoqbot-app[bot]
Reviewed-by: gares Reviewed-by: ejgallego
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-12Fixed grammar productions for PDF documentationsIsaac Oscar Gariano
This undoes changes by 48bb58156acec84991a9e570e93a4e31c0349e79 that broke the rendering of grammar productions in PDfs.
2021-03-11Add deriving lib to CI.Arthur Azevedo de Amorim
2021-03-11noglob/dumpglob should be in coqc specific usageGaëtan Gilbert
Fix #13930
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 23:05:21 +0000