aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-05-14Extract type casts from Gallina.Théo Zimmermann
2020-05-14Merge PR #12214: nit: don't open Persistent_cache in micromegaVincent Laporte
Reviewed-by: vbgl
2020-05-14Add changelog for #12323.Hugo Herbelin
2020-05-14Fixes #12322 (anomaly when printing "fun" binders with implicit types).Hugo Herbelin
A pattern-matching clause was missing in 5f314036e4d (PR #11261). The anomaly triggered in configurations like "fun (x:T) y => ..." (even in the absence of "Implicit Types").
2020-05-14[ci] [sf] Fix SF build.Emilio Jesus Gallego Arias
We move from the previous complex CI download setup to a much more straightforward public mirror repository. Thanks to Yishuai Li and Benjamin Pierce for the very quick response. Closes #12290
2020-05-14Merge PR #12097: Interleave commandline require/set/unset commandsEmilio Jesus Gallego Arias
Ack-by: Zimmi48 Reviewed-by: ejgallego
2020-05-14Merge PR #8808: Extending support for mixing binders and terms in abbreviationsEmilio Jesus Gallego Arias
Ack-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: mattam82
2020-05-14Merge PR #12315: Tests for bugs #9583 (fixed by #11613) and #9679.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-14Merge PR #12244: Store the OCaml version used for Coq in vo files.Emilio Jesus Gallego Arias
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 17:41:33 +0000