coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Amélioration des messages d'erreurs de tacred; unfold considère maintenant le	herbelin	2006-02-07
*	Mise en conformité de l'ordre des occurrences de pattern avec l'affichage	herbelin	2006-02-07
*	Changement des named_context	gregoire	2005-12-02
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Sur le conseil de X.Leroy: x=[\|\|] devient Array.length x=0	letouzey	2005-08-19
*	Added subtac contrib.	coq	2005-05-25
*	Ajout it_mkNamedProd_wo_LetIn	herbelin	2005-02-18
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)	herbelin	2004-08-24
*	Nouvelle en-tête	herbelin	2004-07-16
*	preparation pour release (suite)	barras	2004-03-15
*	Deplacement array_map_left and co dans Util	herbelin	2004-02-13
*	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin	2003-11-24
*	Deplacement de iter_constr_with_full_binders dans Termops	herbelin	2003-10-22
*	Deplacement next_global_ident_away dans Termops	herbelin	2003-10-13
*	Le nom '_' n'est plus valable en v8 pour nommer les variables	herbelin	2003-10-02
*	Changement de l'afficheur pour que les variables liées aient un nom indépen...	herbelin	2003-09-23
*	Deplacement de Declare vers Termops	herbelin	2003-09-13
*	Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...	herbelin	2003-09-12
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	* empty log message *	barras	2003-03-12
*	Prise en compte application partielle dans dependent	herbelin	2002-12-23
*	Petit netoyage dans lib	coq	2002-12-19
*	Allègement du noyau	herbelin	2002-11-18
*	nom de fonction plus simple	barras	2002-10-15
*	retour en arriere concernant la recherche d'occurence modulo expansion des le...	barras	2002-10-09
*	correction de bugs:	barras	2002-08-16
*	Renoncement à distinguer les types "constr" et "types"; nettoyage	herbelin	2002-08-13
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Prise en compte des dependances dans la tactique Case	mohring	2002-03-26
*	Décomposition de l'application n-aire en application binaire pour que Patter...	herbelin	2002-03-21
*	Nouveau Rewrite-in plus economique	barras	2002-03-04
*	petits changements cosmetiques sur les tactiques	barras	2002-02-15
*	substitution et pattern modulo let	barras	2002-02-11
*	petit nettoyage de kernel/inductive	barras	2002-02-07
*	Amélioration affichage échec lookup_eliminator	herbelin	2002-01-17
*	compat ocaml 3.03	filliatr	2001-12-13
*	Suites modifs du noyau. Univ devient purement fonctionnel.	barras	2001-11-12
*	GROS COMMIT:	barras	2001-11-05