coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Finalement un seul constr pour l'instant dans ExtraRedExpr	herbelin	2002-05-30
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	syntax/PPTactic.v passe au niveau ML	herbelin	2002-05-29
*	Déplacement de proofs vers tactics	herbelin	2002-05-29
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Introduction de syntaxe convivial +,*,<=,<,>=	herbelin	2002-05-29
*	Double Induction prend maintenant des noms d'hyppthèses	herbelin	2002-05-29
*	Utilisation d'Infix/Distfix autant que possible	herbelin	2002-05-29
*	Contournement des My_special_variable	herbelin	2002-05-29
*	* empty log message *	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
*	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