coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot
2014-05-06	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-14	Closing bug #3260	Julien Forest
2014-03-19	Adding a Print Strategy vernacular command. It allows to check the	Pierre-Marie Pédrot
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2014-03-02	Migrate back g_obligations in toplevel	Pierre Letouzey
2014-02-24	Simpl_behaviour becomes Reductionops.ReductionBehaviour	Pierre Boutillier
2014-02-16	Removing non-marshallable data from the Agram constructor. Instead of	Pierre-Marie Pédrot
2014-02-02	Removing the [Require "file"] syntax.	Pierre-Marie Pédrot
2014-01-30	G_xml: remove some duplication in error fonctions	Pierre Letouzey
2014-01-30	G_xml: protect against some possible Not_found	Pierre Letouzey
2014-01-13	Documenting old but useful command "Print Tables".	Hugo Herbelin
2014-01-10	Fixing bug #3144.	Pierre-Marie Pédrot
2014-01-05	Proof_using: new syntax + suggestion	Enrico Tassi
2013-12-19	Removing the useless pattern ident genarg.	Pierre-Marie Pédrot
2013-12-12	Patch for supporting [From Xxx Require Yyy Zzz.]	Gregory Malecha
2013-12-04	Vernac classification: allow for commands which start proofs but must be sync...	Arnaud Spiwack
2013-11-30	Getting rid of casted_open_constr. It was only used by the	Pierre-Marie Pédrot
2013-11-27	Actually adding the grammar entry to handle tactics in terms.	Pierre-Marie Pédrot
2013-11-27	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot
2013-11-10	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot
2013-11-09	Revert the previous commit. It broke Coq compilation.	ppedrot
2013-11-09	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot
2013-11-09	Moving notation types into grammar rule.	ppedrot
2013-11-09	Cleaning and documenting Egramcoq.	ppedrot
2013-11-03	empty token in terminal is a user error not an anomaly (bug 3118)	pboutill
2013-11-02	Adds an experimental exactly_once tactical.	aspiwack
2013-11-02	Adds a tactical once.	aspiwack
2013-11-02	Added the tactical "tac1 + tac2".	aspiwack
2013-11-02	Fixes parsing of all: followed by a typechecking/evaluation command.	aspiwack
2013-11-02	New option Default Goal Selector.	aspiwack
2013-11-02	Adds a new goal selector "all:".	aspiwack
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-10-24	Turn many List.assoc into List.assoc_f	letouzey
2013-10-23	cList.index is now cList.index_f, same for index0	letouzey
2013-10-22	Removing some generic equalities.	ppedrot
2013-10-10	STM: add "Stm Wait" to wait for the slaves to complete their jobs	gareuselesinge
2013-10-07	STM: new command "Stm PrintDag" to force printing the dag to /tmp	gareuselesinge
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-09-07	Change syntax of Hint Resolve to actually accept user-given priorities.	msozeau
2013-09-02	* parsing/Lexer: Cosmetics.	regisgia
2013-08-25	Added a more efficient way to recover the domain of a map.	ppedrot
2013-08-19	Modulification and removing of structural equality in Stateid.	ppedrot
2013-08-08	Vernac classification streamlined (handles VERNAC EXTEND)	gareuselesinge
2013-08-08	Support Proof General	gareuselesinge
2013-08-08	State Transaction Machine	gareuselesinge
2013-08-01	Added a Print Debug GC command that displays the current state of	ppedrot