coq - The formal proof system

Age	Commit message (Expand)	Author
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
2001-03-15	entetes	filliatr
2001-03-01	backtrack unification types et deplacement make_clenv_binding	filliatr
2001-02-01	application patch Cuit Alvarado : tclTHENSi et intros_until_n exportés	filliatr
2001-01-31	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr
2001-01-24	Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...	herbelin
2000-12-18	Renommages autour de NewInduction	herbelin
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-11-26	Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...	herbelin
2000-11-24	Nouveau choix pour l'intros initial	delahaye
2000-10-18	Renommage canonique :	herbelin
2000-10-13	Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...	herbelin
2000-09-10	nettoyage	herbelin
2000-09-10	Suppression de Abst	herbelin
2000-05-16	Retrait du i pour tclTHEN_i et correction bugs Decompose	herbelin
2000-05-05	Achèvement nettoyage Pfedit; ajout intros_replacing	herbelin