aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-03-22Merge PR #13225: Remove useless libobject for Implicit TypePierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-22Merge PR #13905: Inline the refold and tactic_mode flags for the cbn tactic.coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-03-22Merge PR #13961: Implement ! goal selector for Ltac2.coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-03-19Merge PR #13956: Remove useless prefix argument in native compilation.coqbot-app[bot]
Reviewed-by: silene
2021-03-19Remove useless libobject for Implicit TypeGaëtan Gilbert
cache_function is called from add_leaf and after discharging sections, but default_object is section local.
2021-03-19Merge PR #13924: Fix kernel incorrectly assuming the "using" hyps are ↵Pierre-Marie Pédrot
transitively closed Reviewed-by: ppedrot
2021-03-19Merge PR #13730: Lint stdlib with -mangle-names #6coqbot-app[bot]
Reviewed-by: anton-trunov
2021-03-18Implement ! goal selector for Ltac2.Pierre-Marie Pédrot
Fixes #13960: Ltac2 Eval does not work with Set Default Goal Selector "!".
2021-03-18Remove useless prefix argument in native compilation.Pierre-Marie Pédrot
2021-03-17Merge PR #13929: [ci] [gitlab] Remove ad-hoc mathcomp install macroscoqbot-app[bot]
Reviewed-by: gares Reviewed-by: Zimmi48
2021-03-17Merge PR #13938: Fast Ltac2 quoted variable typingcoqbot-app[bot]
Reviewed-by: gares
2021-03-16Merge PR #13920: Adding an Ltac2 API to manipulate inductive types.coqbot-app[bot]
Reviewed-by: JasonGross Ack-by: jfehrle
2021-03-16Slightly richer API allowing to shift the inductive in a block.Pierre-Marie Pédrot
2021-03-16Adding a changelog and registering the new file in the documentation.Pierre-Marie Pédrot
2021-03-16Add tests for the new Ltac2 Ind API.Pierre-Marie Pédrot
2021-03-16Adding an Ltac2 API to manipulate inductive types.Pierre-Marie Pédrot
Fixes #10095: Get list of constructors of Inductive.
2021-03-14Merge PR #13935: Fixed grammar productions for PDF documentationscoqbot-app[bot]
Reviewed-by: jfehrle
2021-03-14[ci] [gitlab] Remove ad-hoc mathcomp install macrosEmilio Jesus Gallego Arias
They should not be necessary today as they date from the shareable pre-artifact epoch, an incur in an slowdown.
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-12Use the new API to prevent retyping of Ltac2 variable quotations.Pierre-Marie Pédrot
Fixes #12785: Ltac2 Performance Overhead.
2021-03-12Move the responsibility of type-checking to the caller for tactic-in-terms.Pierre-Marie Pédrot
Instead of taking a type and checking that the inferred type for the expression is correct, we simply pick an optional constraint and return the type directly in the callback. This prevents having to compute type conversion twice in the special case of Ltac2 variable quotations. This should be 1:1 equivalent to the previous code, we are just moving code around.
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-10Fix kernel incorrectly assuming the "using" hyps are transitively closedGaëtan Gilbert
Fix #13903
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-06Inline the refold and tactic_mode flags for the cbn tactic.Pierre-Marie Pédrot
They were unconditionally set to true, leading to a lot of dead branches.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 18:45:35 +0000