index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2020-05-14
Extract type casts from Gallina.
Théo Zimmermann
2020-05-14
Merge PR #12214: nit: don't open Persistent_cache in micromega
Vincent Laporte
2020-05-14
Add changelog for #12323.
Hugo Herbelin
2020-05-14
Fixes #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-14
Merge PR #12097: Interleave commandline require/set/unset commands
Emilio Jesus Gallego Arias
2020-05-14
Merge PR #8808: Extending support for mixing binders and terms in abbreviations
Emilio Jesus Gallego Arias
2020-05-14
Merge PR #12315: Tests for bugs #9583 (fixed by #11613) and #9679.
Emilio Jesus Gallego Arias
2020-05-14
Merge PR #12244: Store the OCaml version used for Coq in vo files.
Emilio Jesus Gallego Arias
2020-05-14
Merge doc on extended pattern matching from two origins.
Théo Zimmermann
2020-05-14
Move extended pattern matching to new location.
Théo Zimmermann
2020-05-13
Add section on pattern matching from Gallina ext.
Théo Zimmermann
2020-05-13
Extract extended pattern matching from Gallina extensions.
Théo Zimmermann
2020-05-13
New file on existential variables.
Théo Zimmermann
2020-05-13
Extract evars from Gallina extensions.
Théo Zimmermann
2020-05-13
Preserve sections about typing rules in CIC chapter.
Théo Zimmermann
2020-05-13
Merge doc of modules from two origins.
Théo Zimmermann
2020-05-13
Move file on modules in new location.
Théo Zimmermann
2020-05-13
Add to file on modules.
Théo Zimmermann
2020-05-13
Extract modules from Gallina ext.
Théo Zimmermann
2020-05-13
New file on primitive objects.
Théo Zimmermann
2020-05-13
Extract primitive objects from Gallina ext.
Théo Zimmermann
2020-05-13
Create a new file on conversion.
Théo Zimmermann
2020-05-13
Extract conversion rules from CIC.
Théo Zimmermann
2020-05-13
Merge sections on CoInductive types and co-recursive functions in new file.
Théo Zimmermann
2020-05-13
Add cofix and CoFixpoint to file on CoInductive types.
Théo Zimmermann
2020-05-13
Extract cofix and CoFixpoint from Gallina.
Théo Zimmermann
2020-05-13
Create new file on CoInductive types.
Théo Zimmermann
2020-05-13
Extract CoInductive types from Gallina.
Théo Zimmermann
2020-05-13
Adding change log for #8808.
Hugo Herbelin
2020-05-13
Overlay elpi
Hugo Herbelin
2020-05-13
Documenting notations with both terms and binders.
Hugo Herbelin
2020-05-13
Extending support for mixing binders and terms in abbreviations.
Hugo Herbelin
2020-05-13
Tests for bugs #9583 (fixed by #11613) and #9679.
Hugo Herbelin
2020-05-13
Merge section on Inductive types from Gallina and CIC.
Théo Zimmermann
2020-05-13
Create new file on Inductive types.
Théo Zimmermann
2020-05-13
Extract Inductive types from CIC.
Théo Zimmermann
2020-05-13
Merge sections on Inductive types and Recursive functions in new file.
Théo Zimmermann
2020-05-13
Add Recursive functions to new file on Inductive types.
Théo Zimmermann
2020-05-13
Extract Recursive functions from Gallina.
Théo Zimmermann
2020-05-13
Create new file on Inductive types.
Théo Zimmermann
2020-05-13
Extract Inductive types from Gallina.
Théo Zimmermann
2020-05-13
Merge sections on variants and match into new file.
Théo Zimmermann
2020-05-13
Merge sections on Variants and Private inductive types into new file.
Théo Zimmermann
2020-05-13
Add match to new file on Variants.
Théo Zimmermann
2020-05-13
Extract match from Gallina.
Théo Zimmermann
2020-05-13
Create a new file on Variants.
Théo Zimmermann
2020-05-13
Extract Variants from Gallina.
Théo Zimmermann
2020-05-13
Create a new file on Variants.
Théo Zimmermann
2020-05-13
Extract Private inductive types from Gallina.
Théo Zimmermann
[prev]
[next]