coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	Insertion de Red sur chaque atome dans Tauto et Intuition	herbelin	2001-12-19
*	Tentative d'amélioration du résultat de Intuition	herbelin	2001-12-19
*	coq-bugs #12: probleme de metamap resolu	barras	2001-12-18
*	compat ocaml 3.03	filliatr	2001-12-13
*	Parade contre effet indésirable du commit précédent	herbelin	2001-12-06
*	Amélioration nommage hypothèses NewInduction (et incompatibilités)	herbelin	2001-12-06
*	desobfuscation du code de la verif de la condition de garde	barras	2001-11-30
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
*	Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant	herbelin	2001-11-20
*	Diverses petites simplications de la machine de preuves.	clrenard	2001-11-19
*	Suppression des stamps et donc des *_constraints	clrenard	2001-11-12