coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Précisions message d'erreur	herbelin	2004-08-23
*	Distinction location ocaml 3.08 ou pas (suite)	herbelin	2004-07-29
*	Distinction location ocaml 3.08 ou pas	herbelin	2004-07-29
*	Bug tactique fix	herbelin	2004-07-28
*	"Print Setoids" command added.	sacerdot	2004-07-23
*	Abstraction vis à vis de dummy_loc	herbelin	2004-07-20
*	Abstraction vis à vis du type loc pour compatibilité ocaml 3.08	herbelin	2004-07-16
*	Suppression quotify	herbelin	2004-07-16
*	Nouvelle en-tête	herbelin	2004-07-16
*	Branchement sur Util.loc et abstraction vis a vis de dummy_loc	herbelin	2004-07-16
*	Abstraction vis a vis de dummy_loc	herbelin	2004-07-16
*	bugs #667 and #783 (mimick_evar and loc_table on large files)	barras	2004-07-13
*	moved instantiate binding to extratactics	corbinea	2004-06-29
*	efficacite du lexeur	filliatr	2004-06-29
*	more evar stuff	corbinea	2004-06-28
*	Nouvelle syntaxe à la ML pour donner le type ML des extensions d'arguments	herbelin	2004-06-17
*	Affichage de l'opacité par About mais pas par Print (compatibilité coq'art)	herbelin	2004-06-03
*	Affichage de l'opacité dans Print et About	herbelin	2004-06-02
*	Bug affichage ClearBody	herbelin	2004-05-27
*	Bug syntaxe AddPath	herbelin	2004-05-14
*	Ajout entree pour exporter les commentaires en mode -xml	herbelin	2004-03-26
*	Code mort	herbelin	2004-03-25
*	Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...	herbelin	2004-03-17
*	Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...	herbelin	2004-03-17
*	Parsing des V8Notation avec motif recursif en v7	herbelin	2004-03-17
*	Utilisation de '..' pour la notation concrete des motifs recursifs de filtrage	herbelin	2004-03-17
*	Mise en place de motifs récursifs dans Notation; quelques simplifications au...	herbelin	2004-03-17
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'	herbelin	2004-03-03
*	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin	2004-03-02
*	Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...	herbelin	2004-03-02
*	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...	herbelin	2004-03-02