coq - The formal proof system

Age	Commit message (Expand)	Author
2020-09-13	Statically ensure that only polymophic hint terms come with a context.	Pierre-Marie Pédrot
2020-07-26	Merge PR #12573: Hint Opaque/Transparent/Unfold: don't error on Opaque Define...	Pierre-Marie Pédrot
2020-07-23	Hint Opaque/Transparent/Unfold: don't error on opaque constants	Gaëtan Gilbert
2020-07-17	Tweak the warning for arbitrary term hints.	Pierre-Marie Pédrot
2020-06-26	[declare] [api] Removal of duplicated type aliases.	Emilio Jesus Gallego Arias
2020-05-10	No more local reduction functions in Reductionops.	Pierre-Marie Pédrot
2020-05-07	[declare] Merge DeclareDef into Declare	Emilio Jesus Gallego Arias
2020-04-21	[declare] [tactics] Move declare to `vernac`	Emilio Jesus Gallego Arias
2020-04-21	[hints] Move and split Hint Declaration AST to vernac	Emilio Jesus Gallego Arias