coq - The formal proof system

Age	Commit message (Expand)	Author
2018-07-01	Implement uniform parameters in ComInductive	Jasper Hugunin
2018-06-26	Remove Sorts.contents	Gaëtan Gilbert
2018-06-18	Remove reference name type.	Maxime Dénès
2018-06-04	[econstr] Remove some Unsafe.to_constr use.	Emilio Jesus Gallego Arias
2018-05-31	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias
2018-05-25	Remove some occurrences of Evd.empty	Maxime Dénès
2018-05-22	Merge PR #7384: Split Universes	Pierre-Marie Pédrot
2018-05-17	Remove unused argument to solve_constraints_system	Gaëtan Gilbert
2018-05-17	Move solve_constraint_system near its only use site (comInductive)	Gaëtan Gilbert
2018-05-08	[api] Move universe syntax to `Glob_term`	Emilio Jesus Gallego Arias
2018-04-17	Deprecate mixing univ minimization and evm normalization functions.	Gaëtan Gilbert
2018-04-12	Fixing the 3 cases of a "Stream.Error" ended with two periods.	Hugo Herbelin
2018-03-09	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias
2018-03-07	Merge PR #6790: Allow universe declarations for [with Definition].	Maxime Dénès
2018-03-05	Allow universe declarations for [with Definition].	Gaëtan Gilbert
2018-03-05	Merge PR #6855: Update headers following #6543.	Maxime Dénès
2018-02-28	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias
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-11	Use specialized function for inductive subtyping inference.	Gaëtan Gilbert
2018-02-10	Inference of inductive subtyping does not need an evar map.	Gaëtan Gilbert
2018-02-10	Simplification: cumulativity information is variance information.	Gaëtan Gilbert
2017-12-23	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias
2017-12-17	[vernac] Split `command.ml` into separate files.	Emilio Jesus Gallego Arias