coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	* added subst_evaluable_reference	sacerdot	2004-12-07
*	The type Pattern.constr_label was isomorphic to Libnames.global_reference.	sacerdot	2004-12-07
*	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot	2004-11-16
*	simplification de clenv	barras	2004-09-10
*	unification encore...	barras	2004-09-08
*	Nouvelle en-tête	herbelin	2004-07-16
*	Ajout option Local à Hint, Hints et HintDestruct	herbelin	2003-06-14
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	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
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Suppression des local_constraints, des ctxtty et du focus.	clrenard	2001-11-06
*	GROS COMMIT:	barras	2001-11-05
*	entetes	filliatr	2001-03-15
*	Eauto version en largeur	mohring	2001-02-26
*	Prise en compte noms longs dans SuperAuto	herbelin	2001-02-16
*	Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...	herbelin	2001-01-24
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
*	Renommage canonique :	herbelin	2000-10-18
*	Prise en compte de l'env local dans make_apply_entry	herbelin	2000-10-11
*	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin	2000-07-24
*	Ajout du langage de tactiques	delahaye	2000-05-03
*	Déplacement du type reference dans Term	herbelin	2000-04-28
*	Introduction d'un type constr_pattern pour les différents filtrages	herbelin	2000-04-26
*	debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkes	filliatr	1999-12-07
*	premier debugage	filliatr	1999-12-05
*	Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations	filliatr	1999-11-24