coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	slim down a bit genarg.ml (pr_intro_pattern forgotten there)	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Fixing bug #2732 (anomaly when using the tolerance for writing	herbelin	2012-03-18
*	Noise for nothing	pboutill	2012-03-02
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	In "simpl c" and "change c with d", c can be a pattern.	herbelin	2009-12-24
*	Made the interpretation levels rlevel/glevel/tlevel truly phantom	herbelin	2009-12-19
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Generalized the possibility to refer to a global name by a notation	herbelin	2009-09-11
*	- Added two new introduction patterns with the following temptative syntaxes:	herbelin	2009-06-07
*	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin	2008-10-19
*	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin	2008-10-11
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Modification rapide du message d'erreur lorsqu'un _ ne peut être	herbelin	2008-07-18
*	Quelques améliorations des intro patterns:	herbelin	2008-04-04
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	More natural notation for intro pattern: @a -> ?a	glondu	2007-07-09
*	New intro pattern "@A", which generates a fresh name based on A.	glondu	2007-07-06
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	Ajout de la possibilité de faire référence dans certains cas à un nom	herbelin	2007-04-28
*	Suppression du type 'tac dans les abstract_argument_type: devenu inutile	herbelin	2006-11-20
*	Changement du type d'argument 'TacticArgType X' en un type	herbelin	2006-06-08
*	Correction trou de subject-reduction de create_arg dans genarg.mli	herbelin	2006-06-07
*	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin	2006-05-30
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
*	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nom	herbelin	2006-01-16
*	Petite correction nom QuantHypArgType suite suppression traducteur	herbelin	2005-12-26
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin	2005-05-17
*	Restauration type casted_open_constr pour tactique refine car l'unification n...	herbelin	2004-12-09
*	Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...	herbelin	2004-12-06
*	Nouvelle en-tête	herbelin	2004-07-16
*	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin	2004-03-02
*	Généralisation du type ltac Identifier en IntroPattern; prise en compte des...	herbelin	2004-03-01
*	Nouvelle tactique EExists	clrenard	2003-12-01
*	New tactics : econstructor, eleft, eright, esplit	clrenard	2003-11-17
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Relachement globalisation Unfold en usage interactif	herbelin	2003-04-10
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14