coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
*	Update headers.	Maxime Dénès	2015-01-12
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Make names in [Proofview_monad] more uniform.	Arnaud Spiwack	2014-10-22
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	Renaming goal-entering functions.	Pierre-Marie Pédrot	2014-09-06
*	Cleaning of the new implementation of the tactic monad.	Arnaud Spiwack	2014-08-04
*	Less use of the list-based interface for goal-bound tactics.	aspiwack	2013-11-02
*	Makes the Ltac debugger usable again.	aspiwack	2013-11-02
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey	2013-03-13
*	invalid_arg instead of raise (Invalid_argement ...)	letouzey	2013-03-12
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (proof)	ppedrot	2012-11-25
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Cleaning Pp.ppnl use	ppedrot	2012-06-01
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
*	Getting rid of Pp.msg	ppedrot	2012-05-30
*	Added documentation for "r foo" in Ltac debugger.	herbelin	2012-01-20
*	Breakpoints in Ltac debugger: new command "r foo" to jump to the next	herbelin	2012-01-20
*	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
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Add possibility to match on defined hypotheses, using brackets to	msozeau	2008-06-16
*	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin	2008-04-01
*	improve the amount of information given by the Ltac tactic debugger	bertot	2006-08-28
*	Protection mode Debug On contre Ctrl-D	herbelin	2006-05-05
*	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin	2006-01-21
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
*	Suppression de la dépendance en Tacmach pour pouvoir être appelé de top_pr...	herbelin	2004-12-31
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	deplacement de clenv vers pretyping	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...	herbelin	2003-06-10
*	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...	herbelin	2003-05-21
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Ajout d'un message à FailTac	herbelin	2003-03-31
*	Debugger plus informatif	delahaye	2003-02-13
*	Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueur	herbelin	2003-01-21
*	Erreur sur precedent commit	herbelin	2003-01-19
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	compat ocaml 3.03	filliatr	2001-12-13
*	Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR	delahaye	2001-10-23
*	entetes	filliatr	2001-03-15