coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23
*	Removing tactic compatibility layer from Elim.	Pierre-Marie Pédrot	2014-04-22
*	Simplifying interface of elimination tactics. They used dummy clausenvs, and	Pierre-Marie Pédrot	2014-04-22
*	Define Tactics.bring_hyps in the new monad.	Pierre-Marie Pédrot	2014-03-28
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Fixing pervasive equalities. In particular, I removed the code that deleted	Pierre-Marie Pédrot	2014-03-03
*	Proofview.Notations: Now that (>>=) is free, use it for tclBIND.	Arnaud Spiwack	2014-02-27
*	Writing [cut] tactic using the new monad.	Pierre-Marie Pédrot	2013-12-02
*	Less use of the list-based interface for goal-bound tactics.	aspiwack	2013-11-02
*	Tachmach.New is now in Proofview.Goal.enter style.	aspiwack	2013-11-02
*	Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).	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-11-02
*	Modulification of identifier	ppedrot	2012-12-14
*	still some more dead code removal	letouzey	2012-10-06
*	remove Refiner.abstract_tactic and similar	letouzey	2012-10-06
*	Clean-up : removal of Proof_type.tactic_expr	letouzey	2012-10-06
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
*	Tacexpr as a mli-only, the few functions there are now in Tacops	letouzey	2012-05-29
*	Noise for nothing	pboutill	2012-03-02
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Generic support for open terms in tactics	herbelin	2009-12-21
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Cleaning/uniformizing the interface of tacticals.mli	herbelin	2009-03-14
*	- Fixed bugs and compatibilities issues in	herbelin	2008-12-30
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Nouvelle en-tête	herbelin	2004-07-16
*	Déplacement définition intro_pattern_expr dans Genarg	herbelin	2004-03-01
*	Bug Double Inversion	herbelin	2003-10-27
*	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin	2003-10-10
*	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin	2003-06-13
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	code mort	herbelin	2003-04-07
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	petits changements cosmetiques sur les tactiques	barras	2002-02-15
*	petit nettoyage de kernel/inductive	barras	2002-02-07
*	Ajout tactiques Rename et Pose; modifications pour Inversion	herbelin	2002-02-01