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
2020-11-26
[vernac] Allow to control typing flags with attributes.
Emilio Jesus Gallego Arias
2020-11-02
attribute #[using] for Definition and Fixpoint
Enrico Tassi
2020-06-26
[declare] [api] Removal of duplicated type aliases.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Move proof information to declare.
Emilio Jesus Gallego Arias
2020-05-09
Merge PR #12241: [declare] Merge DeclareDef into Declare
Gaëtan Gilbert
2020-05-07
[declare] Merge DeclareDef into Declare
Emilio Jesus Gallego Arias
2020-05-01
Warn when a (co)fixpoint is not truly recursive.
Hugo Herbelin
2020-03-30
[comFixpoint] Minor cleanups in type declarations.
Emilio Jesus Gallego Arias
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-07-23
[vernacexpr] Remove duplicate fixpoint record.
Emilio Jesus Gallego Arias
2019-07-23
[vernacexpr] Refactor fixpoint AST.
Emilio Jesus Gallego Arias
2019-06-24
[api] Move `locality` from `library` to `vernac`.
Emilio Jesus Gallego Arias
2019-06-24
[lemmas] [proof] Split proof kinds into per-layer components.
Emilio Jesus Gallego Arias
2019-06-24
[fixpoint] Remove code duplication in (co) fixpoint declaration.
Emilio Jesus Gallego Arias
2019-06-20
Merge PR #9645: [proof] Remove terminator type, unifying regular and obligati...
Pierre-Marie Pédrot
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-17
[proof] drop parameter from terminator type
Emilio Jesus Gallego Arias
2019-06-16
Adding location in warning telling implicit arguments differ in term and type.
Hugo Herbelin
2019-06-09
[proof] Move proofs that have an associated constant to `Lemmas`
Emilio Jesus Gallego Arias
2019-06-04
remove leftover comments
Enrico Tassi
2019-06-04
[vernac] more precise types for Add Morph, Instance, and Function
Enrico Tassi
2019-06-04
Rename Proof_global.{pstate -> t}
Gaëtan Gilbert
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
