aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-03-23Merge PR #13978: Do not match on record types with mutable fields in ↵coqbot-app[bot]
function arguments. Reviewed-by: gares
2021-03-23fix documentation of Ltac2.Env.expandSamuel Gruetter
2021-03-23Fix debug printersGaëtan Gilbert
2021-03-23Merge PR #13974: [cbn internal] env is a regular positional argumentPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-23Do not match on record types with mutable fields in function arguments.Guillaume Melquiond
This tends to confuse the OCaml compiler, for good reasons. Indeed, if there are mutable fields, the generated code cannot wait for the function to be fully applied. It needs to recover the value of the mutable fields as early as possible, and thus to create a closure. Example: let foo {bar} x = ... is compiled as let foo y = match y with {bar} -> fun x -> ...
2021-03-23add lemmas to List.v: Exists_map, Exists_concat, Exists_flat_map, ↵Andrej Dudenhefner
Forall_map, Forall_concat, Forall_flat_map, nth_error_map, nth_repeat, nth_error_repeat
2021-03-23Merge PR #13671: [stdlib] [Vectors] add results on to_listcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-03-23Merge PR #13804: [stdlib] [List] Add results about count_occcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-03-22Move destRef outside ConstrMap.addBESSON Frederic
2021-03-22Merge PR #13225: Remove useless libobject for Implicit TypePierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-22Factorize goal selector handlingGaëtan Gilbert
As a bonus ltac2 can produce bullet suggestions.
2021-03-22[cbn internal] env is a regular positional argumentGaëtan Gilbert
This is more consistent with other code.
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-19implement is_const, is_var, ... etc and has_evar for Ltac2Samuel Gruetter
Fixes #13963
2021-03-19Merge PR #13956: Remove useless prefix argument in native compilation.coqbot-app[bot]
Reviewed-by: silene
2021-03-19[zify] Index by GlobRef instead constrBESSON Frederic
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
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-16correct changelog #13582Olivier Laurent
2021-03-16add changelogOlivier Laurent
2021-03-16add results on to_listOlivier Laurent
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-13Set the lsb of return addresses on the bytecode interpreter stack.Guillaume Melquiond
This makes it possible to skip the check when scanning the stack for the garbage collector.
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-13Documenting the changes.Pierre-Marie Pédrot
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-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-13Minimize the set of multiple inheritance paths to check for conversionKazuhiko Sakaguchi
The table of coercion classes (`class_tab`) has been extended with information about reachability. The conversion checking of a pair of multiple inheritance paths (of coercions) will be skipped if these paths can be reduced to smaller adjoining pairs of multiple inheritance paths, and this reduction will be determined based on that reachability information.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:49:20 +0000