coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Improving error message when abtraction over goal (abstract_list_all	herbelin	2012-10-04
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Tacexpr as a mli-only, the few functions there are now in Tacops	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Noise for nothing	pboutill	2012-03-02
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Made intros_until and onInductionArg a bit stricter and robust	herbelin	2010-06-13
*	Fixed bug #2135 (second-order unification was raising cryptic message)	herbelin	2010-06-12
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Fixing XML doc (COQ_XML not working as an environment variable).	herbelin	2009-10-24
*	Fixed a bug in the interaction between dEqThen and inject_at_positions	herbelin	2009-09-27
*	Delay the choice of eliminator in destruct/induction until we know if	herbelin	2009-09-27
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	- Added two new introduction patterns with the following temptative syntaxes:	herbelin	2009-06-07
*	Cleaning/uniformizing the interface of tacticals.mli	herbelin	2009-03-14
*	- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).	herbelin	2009-01-11
*	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin	2008-12-31
*	About "apply in":	herbelin	2008-12-09
*	- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in	herbelin	2008-11-09
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Modification rapide du message d'erreur lorsqu'un _ ne peut être	herbelin	2008-07-18
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin	2008-06-21
*	- Un peu de doc, préparation du CHANGES pour la release.	herbelin	2008-04-15
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
*	Quelques améliorations des intro patterns:	herbelin	2008-04-04
*	bug in accessing n-th abstraction	barras	2008-01-18
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	New intro pattern "@A", which generates a fresh name based on A.	glondu	2007-07-06
*	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin	2007-05-22
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq	herbelin	2006-01-16
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Réparation bug #1004; nettoyage	herbelin	2005-09-08
*	Correction bug de dependent_hyps qui ne met pas à jour le type des hyps dép...	herbelin	2005-03-20
*	Restructuration fonctions de réécriture depuis égalité dépendante	herbelin	2004-10-27
*	Simplifications concommitantes à la correction du bug #855	herbelin	2004-09-24
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
*	simplification de clenv	barras	2004-09-10
*	unification encore...	barras	2004-09-08