index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
comInductive.mli
Age
Commit message (
Expand
)
Author
2019-11-26
Fix #11039: proof of False with template poly and nonlinear universes
Gaëtan Gilbert
2019-11-01
Expose universe processing in comInductive.
Jan-Oliver Kaiser
2019-10-25
[vernac] [inductive] Remove unused internal export.
Emilio Jesus Gallego Arias
2019-10-25
[inductive] [declare] Move full inductive declaration to declareInd
Emilio Jesus Gallego Arias
2019-08-26
Make kernel parametric on the lowest universe and fix #9294
Matthieu Sozeau
2019-07-19
[vernac] [inductive] Remove unused functions/exports.
Emilio Jesus Gallego Arias
2019-07-01
[api] Reduce declare_kinds even more.
Emilio Jesus Gallego Arias
2019-06-27
[vernac] Cleanup on interface of Vernacentries
Emilio Jesus Gallego Arias
2019-06-24
[api] Remove `polymorphic` type alias, use labels instead.
Emilio Jesus Gallego Arias
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-02-19
Fix #9595: missing non-primitive-record warning with 0 field record
Gaëtan Gilbert
2018-12-19
warn when using auto template, funind never uses template poly
Gaëtan Gilbert
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-09-19
Fix #7754: universe declarations on mutual inductives
Gaëtan Gilbert
2018-09-13
Add option to control automatic template polymorphism.
Gaëtan Gilbert
2018-09-13
Add explicit atribute for template polymorphism.
Gaëtan Gilbert
2018-07-01
Implement uniform parameters in ComInductive
Jasper Hugunin
2018-05-17
Split off Universes functions dealing with names.
Gaëtan Gilbert
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
2017-12-17
[vernac] Split `command.ml` into separate files.
Emilio Jesus Gallego Arias
