coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	No parentheses around f in 'f \subst{...}'	herbelin	2005-05-26
*	Utilisation du module Buffer; encodage plus rigoureux des symboles en uri	herbelin	2005-05-26
*	Patch to avoid Whelp bug removed.	sacerdot	2005-05-26
*	New command: "Print Ltac qualid" to print user defined tactics.	sacerdot	2005-05-20
*	Interface vers outil de recherche Whelp	herbelin	2005-05-20
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin	2005-05-17
*	Globalisation des Tactic Notation	herbelin	2005-05-15
*	Implementation of a new backtracking system, that allow to go back	coq	2005-04-20
*	Ajout récursif du répertoire COQLIB/user-contrib au chemin de chargement	herbelin	2005-03-11
*	Code mort	herbelin	2005-03-01
*	Keep ClosedSection marker for reset	herbelin	2005-02-20
*	Renaming Print Canonical Structure into Print Canonical Projections	herbelin	2005-02-18
*	Moving centralised discharge into dispatched discharge_function; required to ...	herbelin	2005-02-18
*	Moving centralised discharge into dispatched discharge_function; required to ...	herbelin	2005-02-18
*	Moving centralised discharge into dispatched discharge_function; required to ...	herbelin	2005-02-18
*	Moving centralised discharge into dispatched discharge_function; required to ...	herbelin	2005-02-18
*	Ajout Print Canonical Structures	herbelin	2005-02-12
*	Nettoyage et documentation de Library	herbelin	2005-02-06
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Ajout de la syntaxe du reset label: "BackTo n".	coq	2005-01-14
*	Affichage numéro de l'état de la commande courante pour mode emacs	herbelin	2005-01-14
*	- Module/Declare Module syntax made more uniform:	sacerdot	2005-01-06
*	HUGE COMMIT	sacerdot	2005-01-03
*	Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...	herbelin	2005-01-02
*	Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...	herbelin	2005-01-02
*	Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...	herbelin	2005-01-02
*	Rétablissement d'un vrai Eval sous le contexte des définitions, pas un qui ...	herbelin	2004-12-30
*	Amélioration message localisation constructions et modules	herbelin	2004-12-09
*	Bug (cf #892)	herbelin	2004-12-06
*	Amélioration message d'erreur v8	herbelin	2004-12-03
*	Complétion commit précédent	herbelin	2004-11-29
*	Réduire pour trouver l'arité d'une classe	herbelin	2004-11-26
*	Correction bug Notation: il faut re-déclarer les règles de parsing des nota...	herbelin	2004-11-22
*	compatibility with POWERPC	gregoire	2004-11-22
*	Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIRE	herbelin	2004-11-19
*	New command "Print Rewrite HindDb dbname".	sacerdot	2004-11-17
*	Ajout 'Locate Module'	herbelin	2004-11-17
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	* empty log message *	gregoire	2004-11-12
*	Changement dans les boxed values .	gregoire	2004-11-12
*	Prise en compte des notations récursives dans l'option 'format'	herbelin	2004-11-08
*	Non affichage des notations réduites à une variable	herbelin	2004-10-27
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	Semble raisonnable de distinguer les noms aussi dans cant_apply	herbelin	2004-10-17
*	option -no-hash-consing pour supprimmer le hash-consing	filliatr	2004-10-12
*	Suppression IsConjecture redondant avec Conjectural	herbelin	2004-10-11
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	deplacement de clenv vers pretyping	barras	2004-09-03