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
*	Fichiers tactics/.ml4 remplacent les tactics/.v	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 tactics/.ml4 remplacent les tactics/.v	herbelin	2002-05-29
*	Pour les tactiques dépendant de False	herbelin	2002-05-29
*	Correction of a bug in Intuition (no more decomposition of dependent pairs).	corbinea	2002-05-22
*	Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage de	herbelin	2002-05-15
*	Finalement VTactic est gardé pour y plonger les tactiques ML, le	herbelin	2002-05-15
*	- Changement de l'ordre de filtrage dans "Match Context"	herbelin	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
*	Minor correction of get_lem_name	coq	2002-05-02
*	nettoyage code	courant	2002-05-02
*	Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml	herbelin	2002-04-11
*	* empty log message *	courant	2002-04-08
*	- modifs de la condition de garde pour mieux tenir compte des raisonnements	barras	2002-04-02
*	Simplification de Proof_type.prim_rule	herbelin	2002-03-27
*	Prise en compte des dependances dans la tactique Case	mohring	2002-03-26
*	Intuition ne fait plus de Unfold des constantes (il faut les faire	courant	2002-03-21
*	Intuition now takes an (optional) tactic as parameter. This tactic is	courant	2002-03-20
*	Tauto est maintenant stable par "Intro" :	courant	2002-03-15
*	* empty log message *	mohring	2002-03-13
*	Simplify_eq echouait sur des hypotheses trivial comme O=O	barras	2002-03-07
*	* empty log message *	barras	2002-03-05
*	assert failure avec Conditional Rewrite	barras	2002-03-05
*	suppression de code mort	barras	2002-03-05
*	Nouveau Rewrite-in plus economique	barras	2002-03-04
*	labels appliques dans un ordre incorrect	barras	2002-03-01
*	Uniformisation convert_hyp; correction problème de dépendance dans letin_tac	herbelin	2002-02-28
*	suppression de pop_named	barras	2002-02-22
*	Elim dependente n'appelait pas la bonne fonction pour calculer le predicat	barras	2002-02-19
*	but de CutRewrite <- (assert false)	barras	2002-02-18
*	petits changements cosmetiques sur les tactiques	barras	2002-02-15
*	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras	2002-02-14
*	substitution et pattern modulo let	barras	2002-02-11
*	mauvais comportement de l'inversion vis-a-vis des lets	barras	2002-02-08
*	petit nettoyage de kernel/inductive	barras	2002-02-07
*	Ajout tactiques Rename et Pose; modifications pour Inversion	herbelin	2002-02-01
*	changement generation de schema d'elimination, False_rec est primitif, Constr...	mohring	2002-01-31
*	Remplacement cut_intro par true_cut_anon pour Inversion	herbelin	2002-01-25
*	Bug calcul de la signature incorrecte en présence de letin	herbelin	2002-01-25
*	Remplacement cut_intro par true_cut_anon	herbelin	2002-01-24
*	Bug calcul de la signature incorrecte en présence de letin	herbelin	2002-01-24
*	Bug dépendances en les corps des let-in oubliées	herbelin	2002-01-24
*	Mise de Intros id au format de Intro en forçant aussi la réduction si demandé	herbelin	2002-01-15
*	Mise en place de la réduction sous forme d'implications d'atomes en fn de tête	herbelin	2001-12-20
*	Utilisation de Hnf plutôt que Red	herbelin	2001-12-20
*	Puisque Orelse semble lier moins que THEN, ajout d'un reduce après le Orelse	herbelin	2001-12-19