coq - The formal proof system

Age	Commit message (Expand)	Author
2007-04-02	Extension to the general sequence operator (tactical). Now in addition to ...	emakarov
2007-01-22	Correction du bug #1315:	notin
2006-10-23	bug #1194: normalisation evars a la sortie de focus	barras
2006-10-16	affichage des ... dans les scripts	barras
2006-10-05	revision de la semantique de rewrite ... in <clause>. details dans la doc	letouzey
2006-09-26	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-04-28	Standardisation du nom des méthodes de Evd	herbelin
2006-04-14	replacing whd_betaiotaevar_preserving_vm_cast	jforest
2006-03-01	Correction bug #842 (rename d'une hyp du contexte)	herbelin
2006-01-21	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin
2005-12-05	changement d'egalite pour le named_context_val	gregoire
2005-12-02	Changement des named_context	gregoire
2005-11-04	Confusion assert/error détectée par nouveau warning X de ocaml 3.09	herbelin
2005-04-29	Protection against saving a proof with still non-instantiated evars (cf bug #...	herbelin
2005-04-29	Protection against saving a proof with still non-instantiated evars (cf bug #...	herbelin
2004-12-31	Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac...	herbelin
2004-11-17	Mise en page	herbelin
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-09-15	hiding the meta_map in evar_defs	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-02-26	added breakpoints to help ide	corbinea
2003-12-19	Bug affichage des metas dans un environnement avec definitions locales (bug 277)	herbelin
2003-11-12	Idtac peut prendre un argument à afficher	narboux
2003-11-05	2 espaces en trop	herbelin
2003-11-05	Amelioration de l'afficheur de script structure	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-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-04-07	Affichage des tactiques en v8	herbelin
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2003-03-31	Ajout d'un message à FailTac	herbelin
2002-12-19	simplification de solve_subgoal: n'utilise plus frontier	barras
2002-12-09	Option pour rendre les vérifications du refiner optionnelle	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-11-05	Intégration des modifs de la branche mowgli :	herbelin
2002-07-11	Protection contre l'encapsulage de FailError dans Exc_located (sinon, par exe...	herbelin
2002-05-29	Réorganisation des tclTHEN (cf dev/changements.txt)	herbelin
2002-02-08	prterm -> prterm_env	filliatr
2001-12-13	compat ocaml 3.03	filliatr
2001-12-11	suppression de l'affichage des noeuds Change_evars	barras
2001-11-12	Suppression des stamps et donc des *_constraints	clrenard
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
2001-11-05	GROS COMMIT:	barras
2001-09-21	Problème d'affichage d'un . pour les Local_constraints; remplacement par Idtac	herbelin