coq - The formal proof system

Age	Commit message (Expand)	Author
2003-09-12	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...	herbelin
2003-06-19	Ajout 'Symmetry in Hyp'	herbelin
2003-06-13	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin
2003-05-21	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2003-03-31	Bug pattern_occ_hyp_list	herbelin
2003-03-12	* empty log message *	barras
2002-12-21	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin
2002-12-09	Ajout Simpl et Change sur des sous-termes	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-10-21	Ajout d'un suffixe "as [ names ]" pour nommer manuellement les	herbelin
2002-10-21	NewDestruct/NewInduction acceptent l'option "using"	herbelin
2002-05-30	Finalement un seul constr pour l'instant dans ExtraRedExpr	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-03-19	Ajout de l'entrée ne_constrarg_list	delahaye
2002-02-01	Ajout tactiques Rename et Pose; modifications pour Inversion	herbelin
2002-01-31	changement generation de schema d'elimination, False_rec est primitif, Constr...	mohring
2001-12-13	compat ocaml 3.03	filliatr
2001-11-05	GROS COMMIT:	barras
2001-10-05	Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...	herbelin
2001-09-20	Transparent	barras
2001-09-14	Ajout syntaxe "Assert H:T."	herbelin
2001-08-28	Remplace numarg -> pure_numarg dans Double Induction	mohring
2001-08-10	Parsing	herbelin
2001-08-08	Renommage TrueCut -> Assert	herbelin
2001-08-07	Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...	herbelin
2001-08-05	Mise en place d'un nouveau Destruct sur le modèle du nouvel Induction	herbelin
2001-07-02	Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...	herbelin
2001-06-25	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-19	Extension des parametres de Clear + Inst	delahaye
2001-06-18	Interpretation MetaId + Progress + Inst	delahaye
2001-06-11	Fix de quelques bugs syntaxiques de Ltac	delahaye
2001-04-24	Les clauses de Rec doivent prendre des tactic_atom's	delahaye
2001-04-20	Petit menage	delahaye
2001-04-19	* empty log message *	mayero
2001-04-19	Essais dans Ltac	delahaye
2001-04-14	Non parenthesage des applications de tactiques	delahaye
2001-04-12	Ajout de _ dans les patterns d'intro	mohring
2001-04-04	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr
2001-03-15	entetes	filliatr
2001-02-16	Prise en compte noms longs dans SuperAuto	herbelin
2001-02-07	Modif pour les patterns de sous-termes	delahaye
2001-02-01	* empty log message *	mohring
2001-01-31	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr
2000-12-29	Ajout du Let pour le langage de tactiques	delahaye
2000-12-20	ajout ident_or_constrarg pour NewInduction	herbelin
2000-12-19	Correction associativite de Repeat/Orelse	delahaye
2000-12-11	numarg -> pure_numarg a poursuivre	mohring