coq - The formal proof system

Age	Commit message (Expand)	Author
2020-10-27	Rename tac2type -> ltac2_type,	Jim Fehrle
2020-10-26	Ltac2: use ComTactic infrastructure	Gaëtan Gilbert
2020-10-04	Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."	Jim Fehrle
2020-06-26	[declare] Move proof information to declare.	Emilio Jesus Gallego Arias
2020-05-11	Allow to rebind the old value of a mutable Ltac2 entry.	Pierre-Marie Pédrot
2020-04-15	[declare] Rename `Declare.t` to `Declare.Proof.t`	Emilio Jesus Gallego Arias
2020-04-15	[proof] Merge `Pfedit` into proofs.	Emilio Jesus Gallego Arias
2020-04-15	[proof] Merge `Proof_global` into `Declare`	Emilio Jesus Gallego Arias
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-03-03	[exn] Keep information from multiple extra exn handlers	Emilio Jesus Gallego Arias
2020-02-25	Merge PR #11498: [exn] Forbid raising in exn printers, make them return Pp.t ...	Pierre-Marie Pédrot
2020-02-24	[exn] Forbid raising in exn printers, make them return Pp.t option	Emilio Jesus Gallego Arias
2020-02-21	[parsing] Track need to reinit by typing	Emilio Jesus Gallego Arias
2020-02-12	Remove Goptions.opt_name field	Gaëtan Gilbert
2019-11-04	Prevent double definition of Ltac2 constructors inside a module; Fix #11046	Kenji Maillard
2019-11-04	Prevent redefinition of Ltac2 types; fix #10097	Kenji Maillard
2019-11-01	enforcing Ltac2 cosntructors name are uppercase in open types	Kenji Maillard
2019-10-31	enforcing Ltac2 constructor name are uppercased	Kenji Maillard
2019-10-18	Allow to pass Ltac1 values to Ltac2 quotations.	Pierre-Marie Pédrot
2019-07-11	[proof] Minor cleanup in proof.ml	Emilio Jesus Gallego Arias
2019-07-07	[error] Remove special error printing pre-processing	Emilio Jesus Gallego Arias
2019-06-17	Update headers of files that were stuck on older headers.	Théo Zimmermann
2019-06-09	[proof] Uniformize Proof_global API	Emilio Jesus Gallego Arias
2019-06-09	[proof] Move proofs that have an associated constant to `Lemmas`	Emilio Jesus Gallego Arias
2019-06-04	coqpp: add new ![] specifiers for structured proof interaction	Gaëtan Gilbert
2019-05-14	Allow run_tactic to return a value, remove hack from ltac2	Gaëtan Gilbert
2019-05-07	Integrate build and documentation of Ltac2	Maxime Dénès