coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	dans la liste des cmo pour dev/printers.cma, manquait proofs/tacexpr.cmo	letouzey	2006-01-16
*	Restauration des commandes de débogage PrintConstr et PrintPureConstr (suite...	herbelin	2006-01-04
*	Correction dépendance g_prim.ml4/q_coqast.ml4	herbelin	2005-12-30
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin	2005-12-26
*	Achèvement suppression traducteur dans contrib/interface	herbelin	2005-12-26
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Utilisation de -notop pour imposer l'absence de module toplevel	herbelin	2005-12-25
*	Débranchement des parseurs de syntaxe v7	herbelin	2005-12-23
*	Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...	herbelin	2005-12-20
*	correction d'un bug dans le make install	narboux	2005-12-15
*	Changement des named_context	gregoire	2005-12-02
*	commited new ring	barras	2005-11-18
*	Adds tools to help in defining new general recursive functions	bertot	2005-11-07
*	option -w y finalement pas admise par ocamlc <= 3.08.2	herbelin	2005-11-05
*	Compatibilité ocaml 3.09	herbelin	2005-11-04
*	new congruence	corbinea	2005-08-17
*	Subtac: traitement correct des existentielles et de la rÃ©cursion.	coq	2005-07-15
*	reflexive tauto	corbinea	2005-07-15
*	dp: ajout des prédicats de sortes	coq	2005-06-24
*	dp: traitement des fixpoints	coq	2005-06-09
*	Forgot to remove a cmo.	coq	2005-05-25
*	Added subtac contrib.	coq	2005-05-25
*	dp: ajout du prouveur Zenon	coq	2005-05-24
*	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
*	appel de Simplify depuis Coq	coq	2005-03-18
*	tactiques prouveurs premier ordre dans contrib/dp/	coq	2005-03-16
*	Ajout de COQLIB/user-contrib à l'installation pour insister sur la possibili...	herbelin	2005-03-11
*	clean de parser.opt	herbelin	2005-03-01
*	Moving centralised discharge into dispatched discharge_function; required to ...	herbelin	2005-02-18
*	Ajout g_xml.ml4 et cic2Xml.ml	herbelin	2005-02-04
*	Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateurs	herbelin	2005-02-03
*	Application du patch ebuild coq-8.0-r1 de la gentoo (uniformisation du Makefile)	herbelin	2005-02-01
*	Ajout dependance LIBCOQRUN pour coqide et coq-interface	herbelin	2005-01-25
*	Modification cible doc/coq.tex pour tenir des .mli qui n'existent pas toujour...	herbelin	2005-01-21
*	HUGE COMMIT	sacerdot	2005-01-03
*	Pour permettre le chargement des printers en ocamldebug >= 3.07 : renommage s...	herbelin	2005-01-02
*	Remplacement du coeur d'omega (omega.ml) par la version plus générale utili...	herbelin	2004-12-27
*	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin	2004-12-25
*	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot	2004-11-16
*	bug coqmktop avec libcoqrun.a en bytecode	barras	2004-11-15
*	autorewrite moved from HIGHTACTICS to TACTICS (to implement Printing	sacerdot	2004-11-05
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	Tacred après Typing	herbelin	2004-10-18
*	no-assert en mode natif	herbelin	2004-09-26
*	error if binder was already defined	barras	2004-09-23
*	link order again	barras	2004-09-22
*	pbs with link order and deps	barras	2004-09-20
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	repaired deps	barras	2004-09-17