coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Ajout de _ dans les patterns d'intro	mohring	2001-04-12
*	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr	2001-04-04
*	entetes	filliatr	2001-03-15
*	Prise en compte noms longs dans SuperAuto	herbelin	2001-02-16
*	Modif pour les patterns de sous-termes	delahaye	2001-02-07
*	* empty log message *	mohring	2001-02-01
*	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr	2001-01-31
*	Ajout du Let pour le langage de tactiques	delahaye	2000-12-29
*	ajout ident_or_constrarg pour NewInduction	herbelin	2000-12-20