coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-07-02	Moving various ml4 files to mlg.	Pierre-Marie Pédrot

2018-03-08	Make most of TACTIC EXTEND macros runtime calls.	Maxime Dénès
	Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic and its parsing rule. Instead, we make it generate a typed AST that is passed to the parser and a generic tactic execution routine. PMP has written a small parser that can generate the same typed ASTs without relying on camlp5, which is overkill for such simple macros.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2018-02-17	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle
	longer use camlp4.
2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2017-06-10	Remove (useless) aliases from the API.	Matej Košík

2017-06-07	Put all plugins behind an "API".	Matej Kosik

2017-03-24	Merge branch 'trunk' into pr379	Maxime Dénès

2017-03-14	Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun	Maxime Dénès

2017-02-17	Moving the Ltac plugin to a pack-based one.	Pierre-Marie Pédrot
	This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements.
2017-02-16	[cleanup] Change Id.t option to Name.t in TacFun	Tej Chajed

2017-02-14	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot

2016-05-16	Put the "generalize" tactic in the monad.	Pierre-Marie Pédrot

2016-03-06	Splitting the nsatz ML module into an implementation and a grammar files.	Pierre-Marie Pédrot