index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
comFixpoint.mli
Age
Commit message (
Expand
)
Author
2019-06-04
Proof_global: pass only 1 pstate when we don't want the proof stack
Gaëtan Gilbert
2019-04-16
Clean the representation of recursive annotation in Constrexpr
Maxime Dénès
2019-03-27
[vernac] Adapt to removal of imperative proof state.
Emilio Jesus Gallego Arias
2019-03-14
Add relevance marks on binders.
Gaëtan Gilbert
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-11-02
Fixing one instance of bug #8224 (grounding term w/o knowing if it has evars).
Hugo Herbelin
2018-06-27
Swapping Context and Constr: defining declarations on constr in Constr.
Hugo Herbelin
2018-06-12
[api] Misctypes removal: miscellaneous aliases.
Emilio Jesus Gallego Arias
2018-05-31
[api] Move `Constrexpr` to the `interp` module.
Emilio Jesus Gallego Arias
2018-03-07
Merge PR #6790: Allow universe declarations for [with Definition].
Maxime Dénès
2018-03-05
Allow universe declarations for [with Definition].
Gaëtan Gilbert
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-22
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2017-12-17
[vernac] Split `command.ml` into separate files.
Emilio Jesus Gallego Arias
