coq - The formal proof system

Age	Commit message (Expand)	Author
2021-03-25	Fix the redeclaration check for Ltac2 entry points.	Pierre-Marie Pédrot
2021-03-10	Allow to register deprecation status in Ltac2 term and notation declarations.	Pierre-Marie Pédrot
2020-11-30	Add an abstraction function in the LtacX FFI.	Pierre-Marie Pédrot
2020-11-25	Separate interning and pretyping of universes	Gaëtan Gilbert
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-11-04	Prevent double definition of Ltac2 constructors inside a module; Fix #11046	Kenji Maillard
2019-10-31	enforcing Ltac2 constructor name are uppercased	Kenji Maillard
2019-10-29	Fix #10615: Notation substitution for Ltac2 terms.	Pierre-Marie Pédrot
2019-10-18	Allow to pass Ltac1 values to Ltac2 quotations.	Pierre-Marie Pédrot
2019-06-17	Update headers of files that were stuck on older headers.	Théo Zimmermann
2019-05-07	Integrate build and documentation of Ltac2	Maxime Dénès