coq - The formal proof system

Age	Commit message (Expand)	Author
2018-11-05	Port to coqpp.	Pierre-Marie Pédrot
2018-10-26	PR 8671: Remove store / goal extra argument	Matthieu Sozeau
2018-10-01	fix deprecation warnings	Yves Bertot
2018-10-01	adapts to master on Oct. 1st 2018, but warnings remain	Yves Bertot
2018-05-30	Merge branch 'remove_constr_of_global'	Yves Bertot
2018-05-30	remove warnings and merge printing function for econstr terms	Yves Bertot
2018-05-30	remove uses of Universes.constr_of_global	Yves Bertot
2018-05-30	this version has no warnings when compiling	Yves Bertot
2018-05-28	Use user printer for terms instead of debug printer	Maxime Dénès
2018-05-11	This version contains documentation for the code of the packing tactic	Yves Bertot
2018-05-11	Adds a tactic that hides the contents of an hypothesis from view	Yves Bertot
2018-05-11	Use the more colloquial EConstr.t type instead of EConstr.constr	Yves Bertot
2018-05-10	This version has type inference performing proofs, using both type classes	Yves Bertot
2018-05-10	finished the example where type class resolution is forced	Yves Bertot
2018-05-09	This version contains an example of using canonical structures so	Yves Bertot
2018-05-09	checkpoint	Yves Bertot
2018-05-09	trying to force the resolution of type classes by using a cast	Yves Bertot
2018-05-09	an example with type classes, but no class inference triggered yet	Yves Bertot
2018-05-09	repackage with an extra ml file, add a usage of new_type_evar	Yves Bertot
2018-05-09	decompose construction of typed term containing evars	Yves Bertot
2018-05-08	intermediary stage with an EConstr containing a hand-made evar, fauty	Yves Bertot