coq - The formal proof system

Age	Commit message (Expand)	Author
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-12-02	Changement des named_context	gregoire
2005-03-22	Ajout de l'axiome du but prouve par la tactique simplifi	coq
2005-03-07	Added 'clear - id' to clear all hypotheses except the ones dependent in the s...	herbelin
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2005-01-02	Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...	herbelin
2004-10-27	Restructuration fonctions de réécriture depuis égalité dépendante; facto...	herbelin
2004-10-14	reflexivity, symmetry, symmetry ... in e transitivity now fall-back	sacerdot
2004-09-12	inclusion de meta_map dans evar_defs	barras
2004-09-08	unification encore...	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-03-02	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...	herbelin
2004-03-01	Correction sur commit précédent : Tactics.cut réduisait de manière inappr...	herbelin
2004-03-01	Déplacement définition intro_pattern_expr dans Genarg	herbelin
2004-01-09	bugs avec Pose et Assert	barras
2003-11-25	Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...	herbelin
2003-11-13	factorisation et generalisation des clauses	barras
2003-10-13	Deplacement next_global_ident_away dans Termops	herbelin
2003-10-10	changement nouvelle syntaxe (pt fixes)	barras
2003-06-19	Ajout 'Symmetry in Hyp'	herbelin
2003-06-13	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-01-25	Un type "standardisé" pour new_hyp	herbelin
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-08-02	Modules dans COQ\!\!\!\!	coq
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-04-11	Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml	herbelin
2002-03-27	Simplification de Proof_type.prim_rule	herbelin
2002-03-04	Nouveau Rewrite-in plus economique	barras
2002-02-28	Uniformisation convert_hyp; correction problème de dépendance dans letin_tac	herbelin
2002-02-15	petits changements cosmetiques sur les tactiques	barras
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
2002-01-25	Remplacement cut_intro par true_cut_anon pour Inversion	herbelin
2002-01-15	Mise de Intros id au format de Intro en forçant aussi la réduction si demandé	herbelin
2001-11-12	Suppression des stamps et donc des *_constraints	clrenard
2001-11-06	Suite de la suppression : enamed_declaration est remplace par evar_map.	clrenard
2001-11-05	GROS COMMIT:	barras
2001-10-15	Export hide_ident_or_numarg_tactic	herbelin
2001-10-11	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin
2001-10-05	Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...	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-04	ajout Show Intro(s)	letouzey
2001-06-25	Les réduction dans les hypothèses s'appliquent maintenant au corps de la d�...	herbelin
2001-03-28	amelioration de la structure des univers	barras