coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Prise en compte dans cut_ident des idents de la form _23 qui sont officiellem...	herbelin	2004-10-12
*	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
*	Nouvelle en-tête	herbelin	2004-07-16
*	bug #780: compilation of several units in the same coqtop process	barras	2004-07-13
*	correspondance des records et noms de champs de records entre un module et sa...	letouzey	2004-06-25
*	MAJ numéro magique	herbelin	2004-04-14
*	Export de l'information si un inductive est un record ou non (pour xml)	herbelin	2004-03-31
*	The XML exportation hook for require is now active for:	sacerdot	2004-03-30
*	Distinction entre declarations internes (p.ex. _subproof) et declarations uti...	herbelin	2004-03-30
*	Crocret xml pour Require	herbelin	2004-03-29
*	Crochets pour exported les sections en xml	herbelin	2004-03-27
*	Memorisation du type de variable (Hyp or Var)	herbelin	2004-03-26
*	preparation packages V8.0-cdrom	barras	2004-03-15
*	Bug de Require multiple	herbelin	2004-01-28
*	meilleure presentation des commentaires du traducteur	barras	2004-01-02
*	Changement numero magique; message d'erreur en cas de mauvaise syntaxe	herbelin	2003-12-23
*	Reset Initial uniquement interactivement	herbelin	2003-12-19
*	name_app accessible a tous dans Nameops	herbelin	2003-12-19
*	Options -strongly-constructive et -strongly-classical	herbelin	2003-10-28
*	Conjecture declare maintenant un axiome; reorganisation VernacDefinition	herbelin	2003-10-23
*	Deplacement de iter_constr_with_full_binders dans Termops	herbelin	2003-10-22
*	Nouvelle fonction cherchant tous les noms d'un suffixe donne	herbelin	2003-10-21
*	Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...	herbelin	2003-10-08
*	Mise en place d'un mecanisme ne chargeant pas les preuves opaques	herbelin	2003-10-08
*	Correction du bug 335 et Export/Require Export dans un module	coq	2003-10-07
*	Fonctions utiles	herbelin	2003-09-23
*	Utilisation de noms dans 'Implicit Arguments [...]'	herbelin	2003-09-23
*	Mise en place d'implicites par noms en v8	herbelin	2003-09-21
*	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...	herbelin	2003-09-12
*	Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...	herbelin	2003-09-12
*	Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...	herbelin	2003-09-12
*	error	herbelin	2003-09-09
*	Export process_module_bindings pour traducteur	herbelin	2003-09-02