coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau	2006-03-22
*	Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...	herbelin	2006-01-21
*	removes several warnings in contrib/interface	bertot	2006-01-11
*	Changement des named_context	gregoire	2005-12-02
*	Added 'clear - id' to clear all hypotheses except the ones dependent in the s...	herbelin	2005-03-07
*	Standardisation of function names about global references (especially, renami...	herbelin	2005-02-18
*	Abstraction vis a vis du type loc pour ocaml 3.08	herbelin	2004-07-18
*	corrects a bug in name reservation, simplifies or_intro, removes dead code	bertot	2004-02-16
*	a new version that uses intro patterns, but the code still needs some cleaning	bertot	2004-02-11
*	factorisation et generalisation des clauses	barras	2003-11-13
*	Bug TacId	herbelin	2003-11-12
*	Deplacement next_global_ident_away dans Termops	herbelin	2003-10-13
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
*	Ajout notation c.(f) en v8 pour les projections de Record	herbelin	2003-06-10
*	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
*	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea	2003-03-31
*	* empty log message *	barras	2003-03-12
*	Corrects the way conjunctions, existential quantifications, and arrows are	bertot	2003-01-24
*	Make proof by pointing work for the new notations of existential quantification.	bertot	2003-01-23
*	removes all references to ctast.ml the Makefile has been updated accordingly.	bertot	2003-01-22
*	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin	2002-12-21
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Un peu (plus) d'ordre dans Nametab...	coq	2002-09-24
*	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
*	Integrating the Ltac language and the Blast tool into the interface	bertot	2001-12-18
*	GROS COMMIT:	barras	2001-11-05
*	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin	2001-10-17
*	reparation	filliatr	2001-10-12
*	Prsing	herbelin	2001-08-10
*	Two constants had been given in the wrong package (Logic_type instead of	bertot	2001-04-07
*	Files that handle the dialogue with the graphical user-interface pcoq.	bertot	2001-04-04