coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- 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
*	Bug affichage des metas dans un environnement avec definitions locales (bug 277)	herbelin	2003-12-19
*	Idtac peut prendre un argument à afficher	narboux	2003-11-12
*	2 espaces en trop	herbelin	2003-11-05
*	Amelioration de l'afficheur de script structure	herbelin	2003-11-05
*	Paramétrisation vis à vis de existential_key	herbelin	2003-09-06
*	Ground update	corbinea	2003-07-08
*	Ground Update.	corbinea	2003-06-20
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Affichage des tactiques en v8	herbelin	2003-04-07
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Ajout d'un message à FailTac	herbelin	2003-03-31
*	simplification de solve_subgoal: n'utilise plus frontier	barras	2002-12-19
*	Option pour rendre les vérifications du refiner optionnelle	herbelin	2002-12-09
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05