aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-01-11Respect print_universes in detype_instanceGaëtan Gilbert
This partially fixes #13732 and matches what we do in detype_sort
2021-01-10Merge PR #13469: Use nat_or_var for fail/gfailPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-09Merge PR #13299: Remember universe instances of constants in notationscoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: herbelin
2021-01-07Use nat_or_var for fail/gfailJim Fehrle
2021-01-07Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... ↵Pierre-Marie Pédrot
at ..." instead) Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-07Merge PR #13718: Move printing and sorting out of AcyclicGraphcoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-01-07Merge PR #13715: [micromega] Add missing support for `implb`Vincent Laporte
Reviewed-by: vbgl
2021-01-06Merge PR #13563: Revival of #9710 (Compact kernel representation of ↵coqbot-app[bot]
pattern-matching) Reviewed-by: mattam82 Reviewed-by: SkySkimmer Ack-by: gares Ack-by: jfehrle
2021-01-06Merge PR #13714: Changelog for 8.13.0coqbot-app[bot]
Reviewed-by: Zimmi48
2021-01-06Further pushing up the printing and sorting of universes.Pierre-Marie Pédrot
We expose the representation function in UGraph and change the printer signature to work over the representation instead of the abstract type. Similarly, the topological sorting algorithm is moved to Vernacentries. It is now even simpler.
2021-01-06[micromega] Add missing support for `implb`BESSON Frederic
2021-01-05Move universe printing out of AcyclicGraph.Pierre-Marie Pédrot
Instead we export a representation function that gives a high-level view of the data structure in terms of constraints.
2021-01-05Merge PR #13716: [doc] tell sphinxcontrib-bibtex which bibtex file to usecoqbot-app[bot]
Reviewed-by: Zimmi48
2021-01-05[doc] tell sphinxcontrib-bibtex which bibtex file to useEnrico Tassi
2021-01-04Remember universe instances of constants in notationsJasper Hugunin
2021-01-04Document the change of case representation.Pierre-Marie Pédrot
2021-01-04Add overlays.Pierre-Marie Pédrot
2021-01-04Try to preserve the old unification behaviour w.r.t. let-ins in branches.Pierre-Marie Pédrot
The infamous whd_betaiota_deltazeta_for_iota_state function is critical for unification, and it seems that eagerly reducing let-bindings appearing in case branches was a bad idea for efficiency. Instead, when try to preserve the old behaviour where a dummy beta-let cut was introduced.
2021-01-04Make detyping more robust w.r.t. case representation.Pierre-Marie Pédrot
Since we have eta-expansion guaranteed by the term representation, we do not have any more to do a little dance to try to recognize eta-expanded branches and return predicate. Still not able to compile the elpi test, but a good step towards it.
2021-01-04Remove redundant univ and parameter info from CaseInvertGaëtan Gilbert
2021-01-04Fix behaviour of destruct after change of case representation.Pierre-Marie Pédrot
We ensure not to generate dummy beta-cuts in case branches generated by destruct. There was seemingly code trying to perform this but in an akward way.
2021-01-04Temporarily deactivating printing check for cases.Pierre-Marie Pédrot
Destruct has changed semantics, but I'd like to see how CI fares so far.
2021-01-04EConstr iterators respect the binding structure of cases.Pierre-Marie Pédrot
Fixes #3166.
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
We store bound variable names instead of functions for both branches and predicate, and we furthermore add the parameters in the node. Let bindings are not taken into account and require an environment lookup for retrieval.
2021-01-04Move the relative linking order of Inductive w.r.t. VM / native.Pierre-Marie Pédrot
We need this file for the upcoming kernel representation change there.
2021-01-04Merge PR #13685: Add a debug printer for fconstr substitutions.coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-01-04Merge PR #13694: Add a test for a complex conversion involving ↵coqbot-app[bot]
pattern-matching with let-bindings Reviewed-by: SkySkimmer
2021-01-04Changelog for 8.13.0Enrico Tassi
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
(use "with ... at ..." instead)
2021-01-01Merge PR #13470: Convert rewriting and proof-mode chapters to prodncoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
2021-01-01Merge PR #13693: [ci] Switch to testing the maintenance branch for Flocq 3.coqbot-app[bot]
Reviewed-by: gares
2020-12-31Adding a test for conversion involving let-bindings in inductive parameters.Pierre-Marie Pédrot
2020-12-31Add a test for a complex conversion involving pattern-matching with ↵Pierre-Marie Pédrot
let-bindings.
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-12-30Merge PR #13692: Fix failing Windows CI builds.coqbot-app[bot]
Reviewed-by: gares
2020-12-30Merge PR #13321: Move evaluable_global_reference from Names to Tacred.coqbot-app[bot]
Reviewed-by: herbelin Ack-by: ejgallego
2020-12-30Merge PR #13682: Fix broken HTML rendering of inference rules (fix #12783).coqbot-app[bot]
Reviewed-by: herbelin
2020-12-30Fix failing Windows CI builds.Théo Zimmermann
Following a recent change in Cygwin. Co-authored-by: Michael Soegtrop <michael.soegtrop@intel.com>
2020-12-30[ci] Switch to testing the maintenance branch for Flocq 3.Théo Zimmermann
This is the version that CompCert will be compatible with for the time being.
2020-12-30Merge PR #13684: Document the -native-compiler optioncoqbot-app[bot]
Reviewed-by: silene Ack-by: Zimmi48 Ack-by: jfehrle
2020-12-29Merge PR #13686: [refman] Clarify meaning of goal in documentation of ↵coqbot-app[bot]
instantiate. Reviewed-by: jfehrle
2020-12-29[refman] Clarify meaning of goal in documentation of instantiate.Théo Zimmermann
2020-12-29Document the -native-compiler optionPierre Roux
2020-12-28Register a printer for fconstr substitutions in the kernel.Pierre-Marie Pédrot
2020-12-28Export a high-level representation of term substitutions.Pierre-Marie Pédrot
2020-12-28Merge PR #13665: Set Python's default output encoding to utf-8coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: palmskog
2020-12-28Merge PR #13662: Fixes #13657: vscoq needs goal uid.coqbot-app[bot]
Reviewed-by: gares
2020-12-28Fix broken HTML rendering of inference rules (fix #12783).Guillaume Melquiond
2020-12-27Merge PR #13659: Make ssr datastructures cpattern and rpattern publiccoqbot-app[bot]
Reviewed-by: gares
2020-12-27Merge PR #13677: CoqIDE: Fix CC reference in makefilecoqbot-app[bot]
Reviewed-by: gares
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 12:08:56 +0000