coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Parseur pour la DTD XML de constr et un peu plus pour les arguments de tactiques	herbelin	2005-02-04
*	Ajout constructeur External pour appel outil externe à Coq	herbelin	2005-02-04
*	Clarification des niveaux pr_constr et pr_lconstr en v8 dans pr_prim_rule (cu...	herbelin	2005-02-03
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Pour cible make 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
*	Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed	sacerdot	2005-01-14
*	Amélioration message Locate	herbelin	2005-01-13
*	Construct "T with (Definition\|Module) id := c" generalized to	sacerdot	2005-01-13
*	- 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
*	ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...	herbelin	2004-12-29
*	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin	2004-12-25
*	Typo	herbelin	2004-12-24
*	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin	2004-12-24
*	Mecanisme d'affichage des types (notamment les conclusions des buts) typiquem...	herbelin	2004-12-22
*	Restauration type casted_open_constr pour tactique refine car l'unification n...	herbelin	2004-12-09
*	Amélioration message localisation constructions et modules	herbelin	2004-12-09
*	* added subst_evaluable_reference	sacerdot	2004-12-07
*	The type Pattern.constr_label was isomorphic to Libnames.global_reference.	sacerdot	2004-12-07
*	Uniformisation du nom d'entrée openconstr en le nom du type open_constr	herbelin	2004-12-06
*	Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...	herbelin	2004-12-06
*	Indépendance vis à vis de Symbols (suite)	herbelin	2004-11-27
*	Bug commit 1.71	herbelin	2004-11-22
*	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
*	'Rewrite' mot-clé pour que 'Print Rewrite HintDb' marche	herbelin	2004-11-20
*	New command "Print Rewrite HindDb dbname".	sacerdot	2004-11-17
*	Ajout 'Locate Module'	herbelin	2004-11-17
*	Déclaration de '..' comme mot-clé (résoud bug #856)	herbelin	2004-11-17
*	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot	2004-11-16
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	Changement dans les boxed values .	gregoire	2004-11-12
*	Correction bug #868	herbelin	2004-11-10
*	Univ.pr_univ ==> Univ.pr_uni	sacerdot	2004-11-04
*	Affichage des univers	herbelin	2004-11-04
*	Bug mauvais nom d'entrée binder_constr quand récursion gauche	herbelin	2004-10-27
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	Desactivation de la construction 'lazy match' en attendant une autre solution	herbelin	2004-10-12
*	Mise en conformité de la syntaxe de Theorem/Lemma avec la doc: les lieurs so...	herbelin	2004-10-12
*	Réinstallation des lieurs avant l'énoncé de Theorem/Lemma (non documenté ...	herbelin	2004-10-12
*	'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...	herbelin	2004-10-11
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	Ajout de or-pattern pour le match-with v8	herbelin	2004-09-09
*	Meilleur anglais (cf #841)	herbelin	2004-09-08
*	deplacement de clenv vers pretyping	barras	2004-09-03
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Dépendance en pa_ifdef dans la ligne camlp4deps de q_coqast induit make depe...	herbelin	2004-08-26