aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2020-05-14Merge PR #12097: Interleave commandline require/set/unset commandsEmilio Jesus Gallego Arias
Ack-by: Zimmi48 Reviewed-by: ejgallego
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
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-13Documenting notations with both terms and binders.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
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-13Added change log.Hugo Herbelin
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-13Document the changes regarding the order of command-line options.Théo Zimmermann
2020-05-12Merge PR #12309: Remove documentation of -compile, which was removed in #8690.Clément Pit-Claudel
2020-05-12Merge PR #11503: Allow to rebind the old value of a mutable Ltac2 entry.Jason Gross
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: kyoDralliam
2020-05-12Merge PR #12223: Locating error again in atomic tactics (fixes #12152)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-05-12Remove documentation of -compile, which was removed in #8690.Théo Zimmermann
2020-05-12Merge PR #12162: Fixing #12161: rename Bool.leb into Bool.leAnton Trunov
Ack-by: Zimmi48 Reviewed-by: anton-trunov
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 12:53:30 +0000