coq - The formal proof system

Age	Commit message (Expand)	Author
2004-09-10	simplification de clenv	barras
2004-09-10	When refining a given term, the primitive refiner used to accepts some casts,	sacerdot
2004-09-08	unification encore...	barras
2004-09-07	deuxieme vague de modifs: evar_defs fonctionnel	barras
2004-09-03	deplacement de clenv vers pretyping	barras
2004-09-03	premiere reorganisation de l\'unification	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-07-13	bugs #667 and #783 (mimick_evar and loc_table on large files)	barras
2004-07-07	bypass w_Define when w_refine-ing	corbinea
2004-06-30	updated printing of evar context (may loop ?)	corbinea
2004-06-29	moved instantiate binding to extratactics	corbinea
2004-06-28	more evar stuff	corbinea
2004-06-26	effective evar refining	corbinea
2004-04-20	Amélioration message d'erreur quand échec unification	clrenard
2004-03-29	Export du type de preuve en cours pour xml	herbelin
2004-03-02	Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...	herbelin
2004-03-02	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...	herbelin
2004-03-01	Déplacement définition intro_pattern_expr dans Genarg	herbelin
2004-02-26	added breakpoints to help ide	corbinea
2004-02-12	Localisation des erreurs d'internalisation des notations de tactiques	herbelin
2004-01-09	bugs avec Pose et Assert	barras
2003-12-19	Bug affichage des metas dans un environnement avec definitions locales (bug 277)	herbelin
2003-12-01	Amélioration du message d'erreur "w_unify"	clrenard
2003-11-25	Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...	herbelin
2003-11-24	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin
2003-11-15	Amelioration du message d'erreur en cas de tentative d'instanciation	clrenard
2003-11-13	factorisation et generalisation des clauses	barras
2003-11-12	Idtac peut prendre un argument à afficher	narboux
2003-11-12	petits changements de syntaxe	barras
2003-11-09	Traduction semantique des InHyp de clause en InHypValue si local def	herbelin
2003-11-09	Ajout pf_apply	herbelin
2003-11-06	Added Instantiate ... in	corbinea
2003-11-05	2 espaces en trop	herbelin
2003-11-05	Amelioration de l'afficheur de script structure	herbelin
2003-10-16	nouvelle syntaxe de ltac	barras
2003-10-10	code mort	herbelin
2003-10-10	pf_get_new_id en provenance de feu wcclausenv	herbelin
2003-10-10	Suppression clenv_change_head que seul Wcclausenv utisait	herbelin
2003-10-10	Cablage en dur de inversion	herbelin
2003-10-10	Gestion en temps constant de la pile des Unfo; affichage des buts par Pfedit ...	herbelin
2003-10-10	changement nouvelle syntaxe (pt fixes)	barras
2003-10-08	Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...	herbelin
2003-09-12	Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...	herbelin
2003-09-12	open superflu	herbelin
2003-09-06	Paramétrisation vis à vis de existential_key	herbelin
2003-07-08	Ground update	corbinea
2003-06-20	Ground Update.	corbinea
2003-06-19	Ajout 'Symmetry in Hyp'	herbelin
2003-06-13	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin
2003-06-10	Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...	herbelin