aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-05-13Move file on modules in new location.Théo Zimmermann
2020-05-13Add to file on modules.Théo Zimmermann
2020-05-13Extract modules from Gallina ext.Théo Zimmermann
2020-05-13New file on primitive objects.Théo Zimmermann
2020-05-13Extract primitive objects from Gallina ext.Théo Zimmermann
2020-05-13Create a new file on conversion.Théo Zimmermann
2020-05-13Extract conversion rules from CIC.Théo Zimmermann
2020-05-13Merge sections on CoInductive types and co-recursive functions in new file.Théo Zimmermann
2020-05-13Add cofix and CoFixpoint to file on CoInductive types.Théo Zimmermann
2020-05-13Extract cofix and CoFixpoint from Gallina.Théo Zimmermann
2020-05-13Create new file on CoInductive types.Théo Zimmermann
2020-05-13Extract CoInductive types from Gallina.Théo Zimmermann
2020-05-13Adding change log for #8808.Hugo Herbelin
2020-05-13Overlay elpiHugo Herbelin
2020-05-13Documenting notations with both terms and binders.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-05-13Extending support for mixing binders and terms in abbreviations.Hugo Herbelin
2020-05-13Tests for bugs #9583 (fixed by #11613) and #9679.Hugo Herbelin
2020-05-13Merge section on Inductive types from Gallina and CIC.Théo Zimmermann
2020-05-13Create new file on Inductive types.Théo Zimmermann
2020-05-13Extract Inductive types from CIC.Théo Zimmermann
2020-05-13Merge sections on Inductive types and Recursive functions in new file.Théo Zimmermann
2020-05-13Add Recursive functions to new file on Inductive types.Théo Zimmermann
2020-05-13Extract Recursive functions from Gallina.Théo Zimmermann
2020-05-13Create new file on Inductive types.Théo Zimmermann
2020-05-13Extract Inductive types from Gallina.Théo Zimmermann
2020-05-13Merge sections on variants and match into new file.Théo Zimmermann
2020-05-13Merge sections on Variants and Private inductive types into new file.Théo Zimmermann
2020-05-13Add match to new file on Variants.Théo Zimmermann
2020-05-13Extract match from Gallina.Théo Zimmermann
2020-05-13Create a new file on Variants.Théo Zimmermann
2020-05-13Extract Variants from Gallina.Théo Zimmermann
2020-05-13Create a new file on Variants.Théo Zimmermann
2020-05-13Extract Private inductive types from Gallina.Théo Zimmermann
2020-05-13Create new file on sorts.Théo Zimmermann
2020-05-13Extract Sorts out of CIC.Théo Zimmermann
2020-05-13Merge PR #12293: Fix timestamp of coqchk manpageThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-13Added change log.Hugo Herbelin
2020-05-13Ssrmatching: Hack to circumvent a hack.Hugo Herbelin
2020-05-13Make explicit that UGraph lower bounds are only of two kinds.Pierre-Marie Pédrot
This makes the invariants in the code clearer, and also highlight this is only required to implement template polymorphic inductive types.
2020-05-13do not re-export ListNotations from Program: kill overlaysAntonio Nikishaev
2020-05-13Merge PR #12229: Hopefully consensual cleaning of keywordsThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: jfehrle Ack-by: ppedrot
2020-05-13Merge PR #11828: [obligations] Deprecated flag cleanupGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2020-05-13Centralize the OCaml version-checking function.Pierre-Marie Pédrot
We tweak the message a bit.
2020-05-13Store the OCaml version used for Coq in vo files.Pierre-Marie Pédrot
2020-05-13Test interleaving of command-line options.Théo Zimmermann
2020-05-13Document the changes regarding the order of command-line options.Théo Zimmermann
2020-05-13Clarify the assignee's role in removing the overlay informationAnton Trunov
2020-05-13Fixes #12233 (wrong printing env in presence of match branches eta-expansion).Hugo Herbelin
At the same time, we propagate the correct binder relevance in detyping. Note that this would be fixed by enforcing the context of branches in the syntax of "Case".
2020-05-13Clarify the documentation for merging PRs with overlaysAnton Trunov
2020-05-12Merge PR #12309: Remove documentation of -compile, which was removed in #8690.Clément Pit-Claudel
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 11:43:43 +0000