coq - The formal proof system

Age	Commit message (Expand)	Author
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey
2009-03-14	Cleaning/uniformizing the interface of tacticals.mli	herbelin
2009-03-04	Backtrack sur la mémoïsation de nf_evar.	aspiwack
2009-02-27	=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...	aspiwack
2009-02-06	pushed evar reduction in kernel	barras
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-12-09	About "apply in":	herbelin
2008-11-23	first attempt to allow Function to deal with dependent pattern matching. This...	jforest
2008-10-26	Fixes and refinements regarding occurrence selection:	herbelin
2008-08-22	- New auto hints for transparency/opacity control, not bound to	msozeau
2008-08-04	Évolutions diverses et variées.	herbelin
2008-06-27	Enhanced discrimination nets implementation, which can now work with	msozeau
2008-06-10	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin
2008-04-25	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin
2008-04-21	- Parameterize unification by two sets of transparent_state, one for open	msozeau
2008-04-12	Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.	msozeau
2008-03-08	correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)	jforest
2007-12-06	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-11-26	minor bug correction in Function	jforest
2007-11-19	Bug in functionnal induction principle generation	jforest
2007-10-03	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin
2007-09-15	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey
2007-08-31	correction bug d'efficacite dans Function	jforest
2007-07-06	extension of the rename tactic: the following is now allowed:	letouzey
2007-05-17	correction de bug dans Function et augmentation de la classe des fonctions su...	jforest
2007-04-28	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin
2007-04-05	Mise en place d'une nouvelle strategie plus efficace pour les preuves de Func...	jforest
2007-02-12	Bug mineur dans la generation des principes d'induction pour Function	jforest
2007-02-11	Correction d'un bug dans la génération des principes d'induction	jforest
2006-11-13	Correction de la seconde partie du bug #1278	jforest
2006-10-28	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin
2006-09-27	Detection des paramettres pour les Functions bien fondees	jforest
2006-08-25	two minor bug corrections in General Recursive Functions	jforest
2006-08-11	Bug corrections in Function.	jforest
2006-08-08	In the old version, recursive functions cannot be declared inside a section	bertot
2006-07-10	+functional inversion now takes the function to invert as an optional argument.	jforest
2006-07-04	- completely new version of "functional inversion" using inversion on	jforest
2006-06-29	forgot a file	jforest
2006-06-06	+ ameliorating the tactic "functional induction"	jforest
2006-05-31	Replacing the old version of "functional induction" with the new one.	jforest
2006-05-23	Error during last commit (coq didn't compile)	jforest
2006-05-23	Correcting a bug with ocaml <= 3.08.3 (Map.fold changing)	jforest
2006-05-07	+ correcting a bug in general recursive function (match e with _ => match f e...	jforest
2006-05-03	Cleanning and factorizing code in funind. Spliting new_arg_principles into to...	jforest