coq - The formal proof system

Age	Commit message (Expand)	Author
2016-01-20	Update copyright headers.	Maxime Dénès
2015-10-20	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot
2015-10-13	Fix some typos.	Guillaume Melquiond
2015-01-12	Update headers.	Maxime Dénès
2014-12-07	Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.	Hugo Herbelin
2014-10-24	Change reduction_of_red_expr to return an e_reduction_function returning	Matthieu Sozeau
2014-10-01	Simpl less (so that cbn will not simpl too much)	Pierre Boutillier
2014-09-06	Renaming goal-entering functions.	Pierre-Marie Pédrot
2014-08-18	Reorganization of tactics:	Hugo Herbelin
2014-06-23	Fix semantics of change p with c to typecheck c at each specific occurrence o...	Matthieu Sozeau
2014-05-12	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-11-02	More Proofview.Goal.enter.	aspiwack
2013-11-02	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack
2013-11-02	Getting rid of Goal.here, and all the related exceptions and combinators.	aspiwack
2013-11-02	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack
2013-10-24	Get rid of polymorphic comparison in "plugins/btauto/refl_btauto.ml".	xclerc
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 9)	letouzey
2012-08-08	Updating headers.	herbelin
2012-06-28	Replace nat indices with positive one in Btauto.	ppedrot
2012-05-29	place all files specific to camlp4 syntax extensions in grammar/	letouzey
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-29	Glob_term now mli-only, operations now in Glob_ops	letouzey
2012-03-14	Everything compiles again.	msozeau
2012-01-30	Added an pattern / occurence syntax for vm_compute.	ppedrot
2012-01-13	Added a Btauto plugin, that solves boolean tautologies.	ppedrot