coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	info_trivial, info_auto, info_eauto, and debug (trivial\|auto)	letouzey	2012-03-30
*	Noise for nothing	pboutill	2012-03-02
*	A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds	letouzey	2011-03-18
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Fix comment	glondu	2010-06-07
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
*	Improved the efficiency of evars traverals thanks to a split of	herbelin	2010-05-13
*	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
*	Attached evar source to the evar_info and add location to tclWITHHOLES errors	herbelin	2009-12-22
*	In "progress", extending the set of evars w/o solving an existing one is	herbelin	2009-12-21
*	Promote evar_defs to evar_map (in Evd)	glondu	2009-11-11
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Use a lazy value for the message in FailError, so that it won't be	msozeau	2009-06-11
*	- Fixing declarative mode in presence of high use of Change_evars nodes	herbelin	2009-05-20
*	Cleaning/uniformizing the interface of tacticals.mli	herbelin	2009-03-14
*	pushed evar reduction in kernel	barras	2009-02-06
*	Really compare evar maps in progress, due to merging in apply and other	msozeau	2009-01-23
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	- Rebranchement backtrack du langage déclaratif dans Coqide	herbelin	2008-07-18
*	fixed catch_failerror + improved progress check + fixed repeat (repeat simpl ...	barras	2008-05-29
*	Move exception-handling code for catching tactics failure	msozeau	2008-05-01
*	Merge with lmamane's private branch:	lmamane	2008-02-22
*	Adding the tactic "instantiate" (without argument), to force the	glondu	2007-12-07
*	Extension to the general sequence operator (tactical). Now in addition to ...	emakarov	2007-04-02
*	Correction du bug #1315:	notin	2007-01-22
*	bug #1194: normalisation evars a la sortie de focus	barras	2006-10-23
*	affichage des ... dans les scripts	barras	2006-10-16
*	revision de la semantique de rewrite ... in <clause>. details dans la doc	letouzey	2006-10-05
*	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras	2006-09-26
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	Standardisation du nom des méthodes de Evd	herbelin	2006-04-28
*	replacing whd_betaiotaevar_preserving_vm_cast	jforest	2006-04-14
*	Correction bug #842 (rename d'une hyp du contexte)	herbelin	2006-03-01
*	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin	2006-01-21
*	changement d'egalite pour le named_context_val	gregoire	2005-12-05
*	Changement des named_context	gregoire	2005-12-02
*	Confusion assert/error détectée par nouveau warning X de ocaml 3.09	herbelin	2005-11-04
*	Protection against saving a proof with still non-instantiated evars (cf bug #...	herbelin	2005-04-29
*	Protection against saving a proof with still non-instantiated evars (cf bug #...	herbelin	2005-04-29
*	Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac...	herbelin	2004-12-31
*	Mise en page	herbelin	2004-11-17
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
*	deplacement de clenv vers pretyping	barras	2004-09-03
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	added breakpoints to help ide	corbinea	2004-02-26