aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-15Fix typo.Thé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-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-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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:42:53 +0000