coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Nombre magique pour la 8.1beta	herbelin	2006-07-13
*	Correction bug #990 (LoadPath et option -R de coqide	notin	2006-05-30
*	Modification de add_glob (support des modules dans Coqdoc)	notin	2006-05-23
*	Clarification role de library_part : renommage en remove_section_part	herbelin	2006-05-23
*	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin	2006-05-23
*	r8931@thot: notin \| 2006-04-28 16:19:38 +0200	notin	2006-04-28
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
*	Ajout chop_dirpath	herbelin	2006-04-27
*	Changement anomaly en failwith dans out_name pour utilisation par map_succeed	herbelin	2006-04-24
*	Nouveau mécanisme pour les modules interactifs : les arguments de	herbelin	2006-04-16
*	Inversion de l'ordre de chargement des objets logiques et non logiques	herbelin	2006-04-15
*	Ajout array_fold_map', list_fold_map' et list_remove_first	herbelin	2006-03-29
*	Modification des propriétés (svn:executable)	notin	2006-03-17
*	Ajout syntaxe concrète Proposition, synonyme de Lemma	herbelin	2006-01-29
*	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin	2006-01-28
*	- Ajout syntaxe concrète Property/Corollary, synonymes de Lemma	herbelin	2006-01-28
*	* empty log message *	barras	2006-01-20
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Tentative de réparation du bug #1025: it seems like that a casted module sho...	herbelin	2005-12-24
*	Vérification qu'un module est ouvert avant d'insérer une déclaration nomm�...	herbelin	2005-12-23
*	Changement des named_context	gregoire	2005-12-02
*	Fonctionnalisation du cache 'compunit' pour réparer correctement le bug #103...	herbelin	2005-11-26
*	bug #909: Top n'est cree que si le contexte est vide	barras	2005-11-23
*	Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)	herbelin	2005-11-21
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Conformité au principe du nouveau warning X de ocaml 3.09	herbelin	2005-11-04
*	Types inductifs parametriques	mohring	2005-11-02
*	Correction bug #1030 (conséquence du commit 1.84 sur le discharge: add_froze...	herbelin	2005-11-01
*	Adoption du nom canonique global_of_constr pour éviter confusion avec type r...	herbelin	2005-05-20
*	Keep ClosedSection marker for reset	herbelin	2005-02-20
*	Moving centralised discharge into dispatched discharge_function; required to ...	herbelin	2005-02-18
*	Standardisation of constr_of_reference into constr_of_global + Moved Indmap a...	herbelin	2005-02-18
*	Code mort	herbelin	2005-02-18
*	Ajout du reset des numéros d'états dans reset_initial. Plus propre	coq	2005-02-10
*	Nettoyage et documentation de Library	herbelin	2005-02-06
*	Localisation des libraries compilées uniquement via la structure du loadpath...	herbelin	2005-02-05
*	Petit changement dans la gestion des nouveaux labels d'état (pour le	coq	2005-01-31
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed	sacerdot	2005-01-14
*	Ajout mémorisation numéro commande courante + reset vers ce numéro pour mo...	herbelin	2005-01-14
*	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
*	Bug 'Locate Library lib' quand 'lib' est aussi un module	herbelin	2004-11-17
*	dead (and obsolete) code (in comments) removed	sacerdot	2004-11-16
*	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
*	code mort	herbelin	2004-11-09
*	COMMITED BYTECODE COMPILER	barras	2004-10-20