coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Added new command "Set Parsing Explicit" for deactivating parsing (and	herbelin	2012-01-20
*	Interp a definition with the implicit arguments of its local context	pboutill	2011-02-10
*	local variables can have implicits locally	pboutill	2011-02-10
*	Data structure telling implicits of local variables is a map in the	pboutill	2011-02-10
*	More comments and less doublons in some mli	pboutill	2011-02-10
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	Simplified the way internalization_data (i.e. bindings of bound vars	herbelin	2010-07-22
*	Constrintern: unified push_name_env and push_loc_name_env; made	herbelin	2010-07-22
*	Switch to American spelling for "internalise" and "internalisation"	herbelin	2010-07-22
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Various minor improvements of comments in mli for ocamldoc	letouzey	2010-04-29
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Backport fixes in Instance declarations to Program Instance.	msozeau	2010-01-28
*	Promote evar_defs to evar_map (in Evd)	glondu	2009-11-11
*	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin	2009-11-11
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Use more consistent resolution parameters in Program and regular typing	msozeau	2009-06-18
*	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau	2009-03-28
*	DISCLAIMER	puech	2009-01-17
*	- Added support for subterm matching in SearchAbout.	herbelin	2008-12-29
*	More factorization of inductive/record and typeclasses: move class	msozeau	2008-11-09
*	Affichage des notations récursives:	herbelin	2008-10-22
*	Add enough information to correctly globalize recursive calls in inductive and	msozeau	2008-09-11
*	Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...	notin	2008-06-25
*	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
*	Finish fix in command where we still lost information on what was a type	msozeau	2008-03-24
*	Do a second pass on the treatment of user-given implicit arguments. Now	msozeau	2008-03-15
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Fix bug in subst_cases_pattern when aliasing recursive notations.	msozeau	2007-07-02
*	Nouveaux changements autour des implicites (notamment suite à	herbelin	2007-05-06
*	Multiples changements autour des implicites :	herbelin	2007-04-29
*	Support for implicit formal argument types in Program ; parse types in type s...	msozeau	2007-03-28
*	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin	2007-02-13
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	Export de fonctions d'interprétation acceptant des evars non résolues	herbelin	2006-09-01
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Restructuration des points d'entrée de Pretyping et Constrintern	herbelin	2005-12-21
*	Conséquences nettoyage pretyping.ml	herbelin	2005-09-09
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Nouvelle en-tête	herbelin	2004-07-16
*	pb facto des Fixpoint + erreur avec -dump-glob et Load	barras	2004-04-17