coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-23	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot
2014-03-26	Removing tactic compatibility layer in Equality.	Pierre-Marie Pédrot
2014-03-26	Moving some tactic code to the new engine.	Pierre-Marie Pédrot
2014-03-05	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-11-02	Clean up a warning.	aspiwack
2013-11-02	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack
2013-07-09	Revising r16550 about providing intro patterns for applying injection:	herbelin
2013-06-02	Making the behavior of "injection ... as ..." more natural:	herbelin
2013-05-12	Use the Hook module here and there.	ppedrot
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-08-08	Updating headers.	herbelin
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	remove many excessive open Util & Errors in mli's	letouzey
2012-05-29	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey
2012-03-02	Noise for nothing	pboutill
2011-06-18	Relaxed the constraint introduced in r14190 that froze the existing	herbelin
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-05-13	Improved the efficiency of evars traverals thanks to a split of	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-12-28	Safer, though ad hoc, approach to re-interpretation of the argument of	herbelin
2009-12-21	Generic support for open terms in tactics	herbelin
2009-12-16	adding an option functional_induction_rewrite_dependent to make functional in...	jforest
2009-12-12	Updated compatibility for rewriting equality proofs that are dependent	herbelin
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-08	Fix the bug-ridden code used to choose leibniz or generalized	msozeau
2009-08-06	Move out JMeq of subst for compatibility (it affects e.g. the	herbelin
2009-07-24	Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"	letouzey
2009-06-30	Add new variants of [rewrite] and [autorewrite] which differ in the	msozeau
2009-04-08	Some dead code removal + cleanups	letouzey
2008-11-05	Port [rewrite] tactics to open terms. Currently no check that evars	msozeau
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-26	Even better test for choosing rewrite or setoid_rewrite.	msozeau
2008-06-21	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin
2008-06-10	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin
2008-04-12	Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.	msozeau
2008-03-07	Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part	msozeau
2008-03-06	Plug the new setoid implemtation in, leaving the original one commented	msozeau
2008-03-01	Rework on rich forms of rewrite	letouzey
2007-07-06	Adding a syntax for "n-ary" rewrite:	letouzey
2007-05-22	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2007-05-17	correction de bug dans Function et augmentation de la classe des fonctions su...	jforest
2007-04-28	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin