coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Réparation de l'interprétation des fermetures (sans casser Field!)	herbelin	2002-06-13
*	Ajout coercion constr vers hyp quantifiée	herbelin	2002-06-06
*	Tentative de réparation d'un bug Omega: une variable de section qui après e...	herbelin	2002-06-06
*	Passage de PatternMatchingFailure vers UserError pour capture par tclFIRST	herbelin	2002-06-06
*	Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...	herbelin	2002-06-05
*	Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...	herbelin	2002-06-05
*	Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...	herbelin	2002-06-05
*	Les VContext ne sont plus des fermetures (temporaire)	delahaye	2002-05-31
*	Nettoyage	herbelin	2002-05-30
*	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