coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...	notin	2008-07-18
*	Enhanced discrimination nets implementation, which can now work with	msozeau	2008-06-27
*	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin	2008-06-21
*	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin	2008-06-10
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	Minor bug correction in recdef	jforest	2008-06-02
*	Improvements on coqdoc by adding more information into .glob	msozeau	2008-05-30
*	Postpone the search for the recursive argument index from the user given	msozeau	2008-05-06
*	menage dans funind + deplaceemnt de recdef dans funind	jforest	2008-04-28
*	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin	2008-04-25
*	Remplacement de l'appel à interp_constr pour globaliser une constante	herbelin	2008-04-24
*	- Parameterize unification by two sets of transparent_state, one for open	msozeau	2008-04-21
*	Désactivation du dumping des notations quand funind appelle les	herbelin	2008-04-12
*	Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.	msozeau	2008-04-12
*	correction of bug 1829	jforest	2008-04-08
*	- Second pass on implementation of let pattern. Parse "let ' par [as x]?	msozeau	2008-03-28
*	Added a function to rebuild an elim scheme from elim_scheme_info. Will	courtieu	2008-03-18
*	Adapt funind to the RLetPattern constructor.	msozeau	2008-03-15
*	Backtrack wrong commit.	courtieu	2008-03-14
*	indentation.	courtieu	2008-03-14
*	trying f	courtieu	2008-03-13
*	correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)	jforest	2008-03-08
*	Merge with lmamane's private branch:	lmamane	2008-02-22
*	Add new LetPattern construct to replace dest. syntax: let\| pat := t in b is b...	msozeau	2008-01-17
*	Correction of bug #1769	jforest	2008-01-09
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack	2007-12-06
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	bug correction in functional inversion principle generation	jforest	2007-11-27
*	minor bug correction in Function	jforest	2007-11-26
*	Bug in functionnal induction principle generation	jforest	2007-11-19
*	Prise en compte des notations "alias" dans la globalisation des coercions.	herbelin	2007-11-08
*	Cleaning code and comment.	courtieu	2007-10-30
*	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