coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey	2007-09-15
*	correction bug d'efficacite dans Function	jforest	2007-08-31
*	Slight cleanup of refl_omega.ml : in particular it uses now list	letouzey	2007-07-11
*	extension of the rename tactic: the following is now allowed:	letouzey	2007-07-06
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	correction de bug dans Function et augmentation de la classe des fonctions su...	jforest	2007-05-17
*	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin	2007-04-28
*	Mise en place d'une nouvelle strategie plus efficace pour les preuves de Func...	jforest	2007-04-05
*	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau	2007-03-19
*	r11153@tannat: jforest \| 2007-03-16 10:25:55 +0100	jforest	2007-03-16
*	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin	2007-02-13
*	Bug mineur dans la generation des principes d'induction pour Function	jforest	2007-02-12
*	Correction d'un bug dans la génération des principes d'induction	jforest	2007-02-11
*	Retour r9310 en attendant mieux	herbelin	2007-02-09
*	Meilleur anglais (cf 9619)	herbelin	2007-02-07
*	Contounement d'un probleme avec la VM dans Function	jforest	2007-01-26
*	Protection contre les warnings 'unused variable' de ocaml 3.09	herbelin	2007-01-19
*	Functional graph merging deals with letins.	courtieu	2006-11-24
*	Fixed the graph merging parameter order.	courtieu	2006-11-24
*	Fixing syntax and parameter order in functional graph merging.	courtieu	2006-11-23
*	Changing merging functional scheme syntax.	courtieu	2006-11-20
*	Small fix in functional graph merging.	courtieu	2006-11-16
*	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-11-13
*	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-28
*	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-27
*	Some fixes in experimental merging of two functional graphs.	courtieu	2006-10-26
*	Experimental merging of two functional graphs.	courtieu	2006-10-26
*	Starting to add a function schemes merging command (not finished, not	courtieu	2006-10-20
*	r9778@tannat: jforest \| 2006-10-13 11:36:37 +0200	jforest	2006-10-13
*	Detection des paramettres pour les Functions bien fondees	jforest	2006-09-27
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	Gestion des arguments implicites dans les Functions bien fondees	jforest	2006-09-19
*	correction of bug #1220	jforest	2006-09-18
*	Message modification in Function	jforest	2006-09-16
*	mise en conformite des messages d'erreur de Function avec la doc.	jforest	2006-09-14
*	Ajout possibilité clause "where" dans co-points fixes	herbelin	2006-09-01
*	two minor bug corrections in General Recursive Functions	jforest	2006-08-25
*	Amelioration des messages d'erreur de Fucntion	jforest	2006-08-24
*	+ timide essai pour le traitement des as dans les patterns lors de la generat...	jforest	2006-08-16
*	working on functional induction automation (tactic finduction and	courtieu	2006-08-15
*	Bug corrections in Function.	jforest	2006-08-11
*	In the old version, recursive functions cannot be declared inside a section	bertot	2006-08-08
*	Code cleaning in Function	jforest	2006-07-18
*	Code cleaning in Function	jforest	2006-07-18
*	bug correction when defining graph of fixpoints/definitions not generated by ...	jforest	2006-07-13