coq - The formal proof system

Age	Commit message (Expand)	Author
2009-12-22	Attached evar source to the evar_info and add location to tclWITHHOLES errors	herbelin
2009-12-21	In "progress", extending the set of evars w/o solving an existing one is	herbelin
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-06-11	Use a lazy value for the message in FailError, so that it won't be	msozeau
2009-05-20	- Fixing declarative mode in presence of high use of Change_evars nodes	herbelin
2009-03-14	Cleaning/uniformizing the interface of tacticals.mli	herbelin
2009-02-06	pushed evar reduction in kernel	barras
2009-01-23	Really compare evar maps in progress, due to merging in apply and other	msozeau
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-18	- Rebranchement backtrack du langage déclaratif dans Coqide	herbelin
2008-05-29	fixed catch_failerror + improved progress check + fixed repeat (repeat simpl ...	barras
2008-05-01	Move exception-handling code for catching tactics failure	msozeau
2008-02-22	Merge with lmamane's private branch:	lmamane
2007-12-07	Adding the tactic "instantiate" (without argument), to force the	glondu
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