aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
2020-05-14Add a changelog for 8.11.2.Pierre-Marie Pédrot
2020-05-14Merge PR #12312: Clarify the documentation for merging PRs with overlaysThéo Zimmermann
2020-05-14Fix title level and a build failure.Théo Zimmermann
2020-05-14Fix conflicts with latest master.Théo Zimmermann
2020-05-14Add some markers of origin.Théo Zimmermann
2020-05-14Reintroduce leftover parts; update index files; small fixes.Théo Zimmermann
2020-05-14Adding changelog.Pierre-Marie Pédrot
2020-05-14Remove an outdated piece of documentation about limitations of unfold.Pierre-Marie Pédrot
2020-05-14Tweak the error message of reference internalization.Pierre-Marie Pédrot
2020-05-14Add test for #11727, which was indirectly fixed by this PR.Pierre-Marie Pédrot
2020-05-14Generalize the interpretation of syntactic notation as reference to their head.Pierre-Marie Pédrot
2020-05-14Move the static check of evaluability in unfold tactic to runtime.Pierre-Marie Pédrot
2020-05-14Added change log.Hugo Herbelin
2020-05-14Fixes #12234 (wrong environment for Show Proof).Hugo Herbelin
2020-05-14Refactoring of the first part of the reference manual.Théo Zimmermann
2020-05-14Preserve Implicit arguments file.Théo Zimmermann
2020-05-14Remove Canonical structures from Implicit arguments.Théo Zimmermann
2020-05-14Merge doc on Canonical structures from two origins.Théo Zimmermann
2020-05-14Merge PR #12313: Make explicit that UGraph lower bounds are only of two kinds.Gaëtan Gilbert
2020-05-14Move Canonical structures file into new location.Théo Zimmermann
2020-05-14Merge PR #12320: [ci] [sf] Fix SF build.Gaëtan Gilbert
2020-05-14Add Canonical structure declarations to Canonical structures file.Théo Zimmermann
2020-05-14Extract Canonical structures from Implicit arguments.Théo Zimmermann
2020-05-14Split Gallina extensions into multiple files.Théo Zimmermann
2020-05-14Split Gallina into multiple files.Théo Zimmermann
2020-05-14Split parts of CIC into multiple files.Théo Zimmermann
2020-05-14Create new file on Functions and Assumptions.Théo Zimmermann
2020-05-14Extract functions and assumptions.Théo Zimmermann
2020-05-14Merge definitions and type casts in same file.Théo Zimmermann
2020-05-14Create new file on Definitions.Théo Zimmermann
2020-05-14Extract Definitions from Gallina.Théo Zimmermann
2020-05-14Add type casts to new Definitions file.Théo Zimmermann
2020-05-14Extract type casts from Gallina.Théo Zimmermann
2020-05-14Merge PR #12214: nit: don't open Persistent_cache in micromegaVincent Laporte
2020-05-14Add changelog for #12323.Hugo Herbelin
2020-05-14Fixes #12322 (anomaly when printing "fun" binders with implicit types).Hugo Herbelin
2020-05-14[ci] [sf] Fix SF build.Emilio Jesus Gallego Arias
2020-05-14Merge PR #12097: Interleave commandline require/set/unset commandsEmilio Jesus Gallego Arias
2020-05-14Merge PR #8808: Extending support for mixing binders and terms in abbreviationsEmilio Jesus Gallego Arias
2020-05-14Merge PR #12315: Tests for bugs #9583 (fixed by #11613) and #9679.Emilio Jesus Gallego Arias
2020-05-14Merge PR #12244: Store the OCaml version used for Coq in vo files.Emilio Jesus Gallego Arias
2020-05-14Merge doc on extended pattern matching from two origins.Théo Zimmermann
2020-05-14Move extended pattern matching to new location.Théo Zimmermann
2020-05-13Add section on pattern matching from Gallina ext.Théo Zimmermann
2020-05-13Extract extended pattern matching from Gallina extensions.Théo Zimmermann
2020-05-13New file on existential variables.Théo Zimmermann
2020-05-13Extract evars from Gallina extensions.Théo Zimmermann
2020-05-13Preserve sections about typing rules in CIC chapter.Théo Zimmermann
2020-05-13Merge doc of modules from two origins.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 04:04:40 +0000