aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-09-08Merge PR #12991: [Small typo] Update match.rstcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-08Update doc/sphinx/language/extensions/match.rstClément Blaudeau
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-09-08[Small typo] Update match.rstClément Blaudeau
Some error messages were merged together
2020-09-08Merge PR #12927: Explain that tactics applied to multiple goals don't ↵coqbot-app[bot]
preserve the order Reviewed-by: Zimmi48 Ack-by: chdoc Ack-by: jfehrle
2020-09-08Merge PR #12954: Fixes a freshness issue with destruct/induction (see ↵Pierre-Marie Pédrot
comment in #12944). Ack-by: RalfJung Ack-by: jashug Reviewed-by: ppedrot
2020-09-08Merge PR #12987: Fix printing of `change` tacticPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-09-07Merge PR #12988: Remove dead code in clenv-generating functions.Hugo Herbelin
Reviewed-by: herbelin
2020-09-07Explain how selectors change the order of goalsJim Fehrle
2020-09-07Remove dead code in clenv-generating functions.Pierre-Marie Pédrot
The *_env functions used to be different, but now they were just redundant with their direct equivalent.
2020-09-06Fix printing of `change` tactic, which was printed as `change_no_check` and ↵Lasse Blaauwbroek
vice versa
2020-09-06Merge PR #12976: Remove clenv chaining in EqualityHugo Herbelin
Reviewed-by: herbelin
2020-09-06Merge PR #12980: Simplify the implementation of ElimHugo Herbelin
Reviewed-by: herbelin
2020-09-04Remove a unused function from the Clenv API.Pierre-Marie Pédrot
2020-09-04Remove the last use of clenv_fchain in Equality.Pierre-Marie Pédrot
Once again, we now statically the type of the argument is the same, so there is no need to call the old unification.
2020-09-04Inline the last use of apply_on_clause in Equality.Pierre-Marie Pédrot
2020-09-04Remove a useless use of clenv_fchain in Equality.Pierre-Marie Pédrot
The clenv was generated to eliminate a negation, but its argument was given immediately and its type statically known to be the same.
2020-09-04Merge PR #12969: CI: build Iris examples instead of lambda-Rustcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-09-04Statically enforce that elim is passed a fully applied inductive type.Pierre-Marie Pédrot
2020-09-04Restrict a spurious call to a reduction to a quantified inductive type.Pierre-Marie Pédrot
Actually the callers of that function only apply it to an applied inductive type.
2020-09-04Defunctionalize the mk_elim creation in Elim.Pierre-Marie Pédrot
2020-09-04Enforce the argument of elim functions to be a variable.Pierre-Marie Pédrot
2020-09-04Merge PR #12893: Fix incorrect debruijn handling when Record calls ↵coqbot-app[bot]
maybe_unify_params_in Reviewed-by: maximedenes
2020-09-04Merge PR #12900: [bench] Also upload the raw timing files, etcPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-09-04Merge PR #12912: Fix algebraic comparison with sprop on one sidePierre-Marie Pédrot
Reviewed-by: mattam82 Reviewed-by: ppedrot
2020-09-03Merge PR #12953: Add :math: around mathcoqbot-app[bot]
Reviewed-by: jfehrle Ack-by: JasonGross
2020-09-03[bench] Only upload some filesJason Gross
We will now also record a listing of all files that we could have uploaded, in case we want to know what's available to upload in the future.
2020-09-03[bench] Also upload the raw timing files, etcJason Gross
2020-09-03Fix incorrect debruijn handling when Record calls maybe_unify_params_inGaëtan Gilbert
Fix #12887
2020-09-03Merge PR #12968: Replace `frozen` by `allowed` evars in evarconv, and delay themPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-09-03Merge PR #12956: Perform an inversion of control in hint validation for eapply.coqbot-app[bot]
Reviewed-by: mattam82 Ack-by: SkySkimmer Ack-by: ppedrot
2020-09-03Merge PR #12876: Namegen.visible_ids: fixing what seems to be typosPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-09-03Merge PR #12973: Random cleanup around the data structures used in EqualityHugo Herbelin
Reviewed-by: herbelin
2020-09-03Merge PR #12899: [bench] Update bench script with better urls and more infoPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-09-03Add Equations overlayMaxime Dénès
2020-09-03Comment AllowedEvars APIMaxime Dénès
2020-09-02More efficient data structure for allowed evarsMaxime Dénès
2020-09-02Abstract type for allowed evarsMaxime Dénès
2020-09-02Replace `frozen` by `allowed` evars in evarconv, and delay themMaxime Dénès
This is a follow-up of #9062, which introduced a discrenpancy between the two unification engines.
2020-09-02Merge PR #12943: Move Elim-specific codeHugo Herbelin
Ack-by: SkySkimmer Reviewed-by: herbelin
2020-09-02Remove the opening of CErrors in Elim.Pierre-Marie Pédrot
2020-09-02Code deduplication in Elim.Pierre-Marie Pédrot
2020-09-02Factorize the only uses of internal API in Elim for Inv.Pierre-Marie Pédrot
2020-09-02Make the Elim.branch_args type opaque.Pierre-Marie Pédrot
2020-09-02Further remove the type Elim.branch_assumptions.Pierre-Marie Pédrot
Only one field was used throughout the code base.
2020-09-02Remove unused API from Elim.Pierre-Marie Pédrot
2020-09-02Document the Equality.equality type in the ML file.Pierre-Marie Pédrot
2020-09-02Remove redundant data from the equality eliminator datatype.Pierre-Marie Pédrot
2020-09-02Do not look for a quantified inductive type in intropattern injection.Pierre-Marie Pédrot
The code below checks that the term is an applied equality, so allowing non-trivially quantified inductive types would trigger an error right after.
2020-09-02Use a dedicated type for equality elimination.Pierre-Marie Pédrot
In this mess of higher-order callbacks it helps sorting out the invariants of the structure.
2020-09-02fix grepping for the Iris commitRalf Jung
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 04:12:25 +0000