coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ajout EVAL	herbelin	2002-05-29
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Réorganisation des tclTHEN (cf dev/changements.txt)	herbelin	2002-05-29
*	Fichiers contrib//.ml4 remplacent les contrib//.v	herbelin	2002-05-29
*	Fichiers tactics/.ml4 remplacent les tactics/.v	herbelin	2002-05-29
*	Pour les tactiques dépendant de False	herbelin	2002-05-29
*	Implante la macro camlp4 VERNAC COMMAND EXTEND	herbelin	2002-05-29
*	Implante la macro camlp4 TACTIC EXTEND	herbelin	2002-05-29
*	Fichier des expressions de commandes vernaculaires	herbelin	2002-05-29
*	Fichier des expressions de tactiques	herbelin	2002-05-29
*	MAJ 7.3	herbelin	2002-05-29
*	Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.v	herbelin	2002-05-29
*	Ajout de Eval, Inst et Check	delahaye	2002-05-27
*	Changement Filename.is_relative en Filename.is_implicit, plus pertinent	herbelin	2002-05-27
*	Oublis	herbelin	2002-05-22
*	* empty log message *	desmettr	2002-05-22
*	* empty log message *	herbelin	2002-05-22
*	Correction of a bug in Intuition (no more decomposition of dependent pairs).	corbinea	2002-05-22
*	Field + MapleMode	delahaye	2002-05-21
*	MAJ	herbelin	2002-05-16
*	ARCH passe de Makefile à config.distrib	herbelin	2002-05-16
*	MAJ	herbelin	2002-05-16
*	MAJ V7.3	herbelin	2002-05-16
*	Ajout Peano_dec et Compare_dec	herbelin	2002-05-16
*	suppression de inf_decidable dans ZArith_dec (pour SeachPattern)	filliatr	2002-05-16
*	Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage de	herbelin	2002-05-15
*	Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage de	herbelin	2002-05-15
*	MAJ	herbelin	2002-05-15
*	Finalement VTactic est gardé pour y plonger les tactiques ML, le	herbelin	2002-05-15
*	- abstract_sum_scalar, plus_sum_scalar and minus_sum_scalar were bogus	barras	2002-05-15
*	Contournement de la fermeture ML dans VContext	herbelin	2002-05-15
*	MAJ	herbelin	2002-05-15
*	MAJ V7.3	herbelin	2002-05-15
*	maj	filliatr	2002-05-15
*	mention -dump-glob	filliatr	2002-05-15
*	MAJ	herbelin	2002-05-14
*	- Changement de l'ordre de filtrage dans "Match Context"	herbelin	2002-05-14
*	Utilisation d'une construction spéciale SECVAR pour gérer la	herbelin	2002-05-14
*	petite erreur de syntaxe	barras	2002-05-14
*	modification de clenv_merge:	barras	2002-05-14
*	Ajout de la modification des sortes d'elimination	mohring	2002-05-14
*	ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewrite	barras	2002-05-14
*	Changement de eq en eqT comme equivalence de setoide par defaut.	clrenard	2002-05-14
*	encore des lemmes sur Zdiv	filliatr	2002-05-14
*	nouveaux lemmes dans Zdiv (Claude Marche)	filliatr	2002-05-14
*	Utilisation des de Bruijn pour la constructions des records et de leur projec...	herbelin	2002-05-13
*	Pas de projection si le nom d'un champ est '_' dans un Record	herbelin	2002-05-13
*	Plus de souplesse pour les constructeurs encapsulés sous des définitions	herbelin	2002-05-10
*	lemmes plus_O_n et plus_Sn_m (pour Yves)	filliatr	2002-05-07
*	lemmes plus_O_n et plus_Sn_m (pour Yves)	filliatr	2002-05-07