coq - The formal proof system

Age	Commit message (Expand)	Author
2008-03-08	correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)	jforest
2008-02-22	Merge with lmamane's private branch:	lmamane
2008-01-17	Add new LetPattern construct to replace dest. syntax: let\| pat := t in b is b...	msozeau
2008-01-09	Correction of bug #1769	jforest
2007-12-31	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau
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-27	bug correction in functional inversion principle generation	jforest
2007-11-26	minor bug correction in Function	jforest
2007-11-19	Bug in functionnal induction principle generation	jforest
2007-11-08	Prise en compte des notations "alias" dans la globalisation des coercions.	herbelin
2007-10-30	Cleaning code and comment.	courtieu
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-11	Slight cleanup of refl_omega.ml : in particular it uses now list	letouzey
2007-07-06	extension of the rename tactic: the following is now allowed:	letouzey
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
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-03-19	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau
2007-03-16	r11153@tannat: jforest \| 2007-03-16 10:25:55 +0100	jforest
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
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
2007-02-09	Retour r9310 en attendant mieux	herbelin
2007-02-07	Meilleur anglais (cf 9619)	herbelin
2007-01-26	Contounement d'un probleme avec la VM dans Function	jforest
2007-01-19	Protection contre les warnings 'unused variable' de ocaml 3.09	herbelin
2006-11-24	Functional graph merging deals with letins.	courtieu
2006-11-24	Fixed the graph merging parameter order.	courtieu
2006-11-23	Fixing syntax and parameter order in functional graph merging.	courtieu
2006-11-20	Changing merging functional scheme syntax.	courtieu
2006-11-16	Small fix in functional graph merging.	courtieu
2006-11-13	Correction de la seconde partie du bug #1278	jforest
2006-11-13	Correction de la premiere partie du #1278 (but non referme en cas d'echec)	jforest
2006-10-28	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin
2006-10-28	Fixes in experimental merging of functional graphs.	courtieu
2006-10-27	Fixes on functional graphs merging: put functional results at the end	courtieu
2006-10-27	Fixes on functional graphs merging: removed debug printing.	courtieu
2006-10-27	Fixes on functional graphs merging: names of constructors.	courtieu
2006-10-26	Some fixes in experimental merging of two functional graphs.	courtieu
2006-10-26	Experimental merging of two functional graphs.	courtieu
2006-10-20	Starting to add a function schemes merging command (not finished, not	courtieu
2006-10-13	r9778@tannat: jforest \| 2006-10-13 11:36:37 +0200	jforest
2006-09-27	Detection des paramettres pour les Functions bien fondees	jforest
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-09-19	Gestion des arguments implicites dans les Functions bien fondees	jforest
2006-09-18	correction of bug #1220	jforest