coq - The formal proof system

Age	Commit message (Expand)	Author
2020-10-29	Use same code for "Print Ltac foo" and "Print foo" when "foo" is an Ltac.	Hugo Herbelin
2020-10-27	Rename misc nonterminals	Jim Fehrle
2020-10-27	Rename tactic_expr -> ltac_expr	Jim Fehrle
2020-10-26	Merge PR #13137: [ltac] Avoid magic numbers	coqbot-app[bot]
2020-10-14	Deprecating wit_var to the benefit of its synonymous wit_hyp.	Hugo Herbelin
2020-10-04	Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."	Jim Fehrle
2020-10-03	Avoid magic numbers	Jim Fehrle
2020-09-22	Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.	Hugo Herbelin
2020-07-01	[state] Consolidate state handling in Vernacstate	Emilio Jesus Gallego Arias
2020-05-07	Add helper API to define low-level Ltac functions.	Pierre-Marie Pédrot
2020-04-13	pass filters around	Gaëtan Gilbert
2020-03-25	[pcoq] Inline the exported Gramlib interface instead of exposing it as G	Emilio Jesus Gallego Arias
2020-03-25	[parsing] Remove extend AST in favor of gramlib constructors	Emilio Jesus Gallego Arias
2020-03-25	[parsing] Make grammar rules private.	Emilio Jesus Gallego Arias
2020-03-25	[parsing] Make grammar extension type private.	Emilio Jesus Gallego Arias
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-02-21	[parsing] Track need to reinit by typing	Emilio Jesus Gallego Arias
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-03-31	Multiple payload types in tokens	Pierre Roux
2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
2018-11-27	[gramlib] Minor cleanups:	Emilio Jesus Gallego Arias
2018-11-21	[legacy proof engine] Remove some cruft.	Emilio Jesus Gallego Arias
2018-11-17	[ltac] Use CAst nodes in the tactic AST.	Emilio Jesus Gallego Arias
2018-11-13	[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.	Emilio Jesus Gallego Arias
2018-10-30	Remove fully_empty_glob_sign which uses a dummy environment	Maxime Dénès
2018-10-15	Providing a centralized API for ARGUMENT EXTEND.	Pierre-Marie Pédrot
2018-10-02	Pass unnamed arguments to ML macros.	Pierre-Marie Pédrot
2018-07-26	Merge PR #8050: Cleanup VERNAC EXTEND	Maxime Dénès
2018-07-12	Statically typecheck the VERNAC EXTEND wrapper.	Pierre-Marie Pédrot
2018-07-12	Tactic deprecation machinery	Maxime Dénès
2018-07-02	Slight simplification of the Tacentries API to register ML tactics.	Pierre-Marie Pédrot
2018-06-29	Use a homebrew parser to replace the GEXTEND extension points of Camlp5.	Pierre-Marie Pédrot
2018-06-18	Remove reference name type.	Maxime Dénès
2018-06-12	[api] Remove Misctypes.	Emilio Jesus Gallego Arias
2018-03-09	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias
2018-03-08	Make most of TACTIC EXTEND macros runtime calls.	Maxime Dénès
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
2018-02-20	Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.	Hugo Herbelin
2017-11-02	Improving checks about the list separator in tactic notations.	Hugo Herbelin
2017-10-17	[stm] Remove state-handling from Futures.	Emilio Jesus Gallego Arias
2017-10-03	Ltac uses the new generic locatable API.	Pierre-Marie Pédrot
2017-10-03	Moving the Ltac-specific part of the nametab to the Ltac plugin.	Pierre-Marie Pédrot
2017-09-19	Allow declaring universe constraints at definition level.	Matthieu Sozeau
2017-07-25	[api] Remove type equalities from API.	Emilio Jesus Gallego Arias
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-05-31	Creating a module Nameops.Name extending module Names.Name.	Hugo Herbelin