coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ajout 'as (x,...,y)' dans NewDestruct et NewInd, NewInduction, ...	herbelin	2004-01-27
*	bugs avec Pose et Assert	barras	2004-01-09
*	meilleure presentation des commentaires du traducteur	barras	2004-01-02
*	Nouvelle tactique EExists	clrenard	2003-12-01
*	Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...	herbelin	2003-11-25
*	New tactics : econstructor, eleft, eright, esplit	clrenard	2003-11-17
*	factorisation et generalisation des clauses	barras	2003-11-13
*	Traduction semantique des InHyp de clause en InHypValue si local def	herbelin	2003-11-09
*	Added Instantiate ... in	corbinea	2003-11-06
*	Cablage en dur de inversion	herbelin	2003-10-10
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
*	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...	herbelin	2003-09-12
*	Ajout 'Symmetry in Hyp'	herbelin	2003-06-19
*	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin	2003-06-13
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Bug pattern_occ_hyp_list	herbelin	2003-03-31
*	* empty log message *	barras	2003-03-12
*	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin	2002-12-21
*	Ajout Simpl et Change sur des sous-termes	herbelin	2002-12-09
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Ajout d'un suffixe "as [ names ]" pour nommer manuellement les	herbelin	2002-10-21
*	NewDestruct/NewInduction acceptent l'option "using"	herbelin	2002-10-21
*	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
*	Ajout de l'entrée ne_constrarg_list	delahaye	2002-03-19
*	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
*	compat ocaml 3.03	filliatr	2001-12-13
*	GROS COMMIT:	barras	2001-11-05
*	Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...	herbelin	2001-10-05
*	Transparent	barras	2001-09-20
*	Ajout syntaxe "Assert H:T."	herbelin	2001-09-14
*	Remplace numarg -> pure_numarg dans Double Induction	mohring	2001-08-28
*	Parsing	herbelin	2001-08-10
*	Renommage TrueCut -> Assert	herbelin	2001-08-08
*	Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...	herbelin	2001-08-07
*	Mise en place d'un nouveau Destruct sur le modèle du nouvel Induction	herbelin	2001-08-05
*	Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...	herbelin	2001-07-02
*	Les réduction dans les hypothèses s'appliquent maintenant au corps de la d�...	herbelin	2001-06-25
*	Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...	herbelin	2001-06-25
*	Extension des parametres de Clear + Inst	delahaye	2001-06-19
*	Interpretation MetaId + Progress + Inst	delahaye	2001-06-18
*	Fix de quelques bugs syntaxiques de Ltac	delahaye	2001-06-11
*	Les clauses de Rec doivent prendre des tactic_atom's	delahaye	2001-04-24
*	Petit menage	delahaye	2001-04-20
*	* empty log message *	mayero	2001-04-19
*	Essais dans Ltac	delahaye	2001-04-19
*	Non parenthesage des applications de tactiques	delahaye	2001-04-14