coq - The formal proof system

Age	Commit message (Expand)	Author
2009-03-20	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey
2009-03-16	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin
2009-03-14	Cleaning/uniformizing the interface of tacticals.mli	herbelin
2009-03-04	commande Timeout + compaction des traces de debug_tactic	barras
2009-02-19	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack
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
2009-01-18	Backporting from v8.2 to trunk:	herbelin
2009-01-04	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-26	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin
2008-12-14	Fix looping class resolution bug discovered by B. Aydemir and use the	msozeau
2008-12-09	About "apply in":	herbelin
2008-11-27	fixing problem with CompCert: reordering resulting from tac change was not cl...	barras
2008-11-26	closed bug 1898: fold x in x; added a reordering primitive tactic	barras
2008-10-26	Fixes and refinements regarding occurrence selection:	herbelin
2008-10-26	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin
2008-10-25	More debugging of handling of open constrs with typeclasses:	msozeau
2008-10-25	Fix for bug #1981, correct the mismatch between the meta types used in	msozeau
2008-10-24	Raise informative errors instead of Failures or anomalies in case a meta	msozeau
2008-10-19	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin
2008-10-18	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin
2008-10-07	fixing r11433 again:	barras
2008-10-06	bug #1951: polymorphic indtypes: universe subst was not performed in the type...	barras
2008-09-09	Correction bug assert (introduit dans la révision 11300) qui ne	herbelin
2008-09-07	More debugging of [Equations], now able to discharge even the heavily	msozeau
2008-08-05	Correction de bugs:	herbelin
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-18	- Rebranchement backtrack du langage déclaratif dans Coqide	herbelin
2008-07-18	Modification rapide du message d'erreur lorsqu'un _ ne peut être	herbelin
2008-06-27	Changement de catch_error pour qu'il rattrape les erreurs d'arguments	aspiwack
2008-06-21	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin
2008-06-16	Add possibility to match on defined hypotheses, using brackets to	msozeau
2008-06-11	Correction de deux bugs liés au commit 11094 sur les clauses "at" et "in".	herbelin
2008-06-10	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin
2008-06-08	- Extension de "generalize" en "generalize c as id at occs".	herbelin
2008-06-03	Fixes incorrect handling of existing existentials variables in	msozeau
2008-05-29	fixed catch_failerror + improved progress check + fixed repeat (repeat simpl ...	barras
2008-05-22	Strategy commands are now exported	barras
2008-05-21	refined the conversion oracle	barras
2008-05-01	Move exception-handling code for catching tactics failure	msozeau
2008-04-30	Réutilisation de l'infrastructure pour le polymorphisme d'univers des	herbelin
2008-04-28	Suite commit 10861	herbelin
2008-04-28	Petites corrections vis à vis des commits 10860, 10859, 10850	herbelin
2008-04-27	- Backtrack sur option with_types suite à confusion sur l'utilisation	herbelin
2008-04-26	- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec	herbelin
2008-04-25	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin
2008-04-23	Prise en compte des coercions dans les clauses "with" même si le type	herbelin
2008-04-21	- Parameterize unification by two sets of transparent_state, one for open	msozeau
2008-04-17	Bug squashing day !	msozeau