index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
/
sphinx
/
language
Age
Commit message (
Expand
)
Author
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
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
2020-05-13
Create new file on sorts.
Théo Zimmermann
2020-05-13
Extract Sorts out of CIC.
Théo Zimmermann
2020-05-13
Merge PR #12229: Hopefully consensual cleaning of keywords
Théo Zimmermann
2020-05-09
[doc] Add hexadecimal numerals
Pierre Roux
2020-05-07
Drop some the coqtop output, rephrase a bit
Quentin Carbonneaux
2020-05-06
Add an example to motivate strictly positive occurrences check
Quentin Carbonneaux
2020-05-06
Keywords: Applying suggestions from Jim Fehrle and Théo Zimmermann.
Hugo Herbelin
2020-05-06
Documenting plugin/tactic/stdlib keywords in corresponding chapters.
Hugo Herbelin
2020-05-01
Move essential vocabulary and syntax conventions to section on basics.
Théo Zimmermann
2020-05-01
Extract two new files out of Gallina chapter.
Théo Zimmermann
2020-05-01
Create section on writing libraries with only deprecated attributes.
Théo Zimmermann
2020-05-01
Extract deprecated attribute from Gallina chapter.
Théo Zimmermann
2020-05-01
Remove lexical conventions and attributes from Gallina chapter.
Théo Zimmermann
2020-05-01
Create basics out of sections from Gallina and Vernac chapters.
Théo Zimmermann
[prev]
[next]