coq - The formal proof system

Age	Commit message (Expand)	Author
2005-01-13	Construct "T with (Definition\|Module) id := c" generalized to	sacerdot
2005-01-06	- Module/Declare Module syntax made more uniform:	sacerdot
2005-01-03	HUGE COMMIT	sacerdot
2005-01-02	Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...	herbelin
2004-11-17	Bug 'Locate Library lib' quand 'lib' est aussi un module	herbelin
2004-11-16	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-09	code mort	herbelin
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-10-12	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-11	Suppression IsConjecture redondant avec Conjectural	herbelin
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-07-13	bug #780: compilation of several units in the same coqtop process	barras
2004-06-25	correspondance des records et noms de champs de records entre un module et sa...	letouzey
2004-04-14	MAJ numéro magique	herbelin
2004-03-31	Export de l'information si un inductive est un record ou non (pour xml)	herbelin
2004-03-30	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-29	Crocret xml pour Require	herbelin
2004-03-27	Crochets pour exported les sections en xml	herbelin
2004-03-26	Memorisation du type de variable (Hyp or Var)	herbelin
2004-03-15	preparation packages V8.0-cdrom	barras
2004-01-28	Bug de Require multiple	herbelin
2004-01-02	meilleure presentation des commentaires du traducteur	barras
2003-12-23	Changement numero magique; message d'erreur en cas de mauvaise syntaxe	herbelin
2003-12-19	Reset Initial uniquement interactivement	herbelin
2003-12-19	name_app accessible a tous dans Nameops	herbelin
2003-10-28	Options -strongly-constructive et -strongly-classical	herbelin
2003-10-23	Conjecture declare maintenant un axiome; reorganisation VernacDefinition	herbelin
2003-10-22	Deplacement de iter_constr_with_full_binders dans Termops	herbelin
2003-10-21	Nouvelle fonction cherchant tous les noms d'un suffixe donne	herbelin
2003-10-08	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-07	Correction du bug 335 et Export/Require Export dans un module	coq
2003-09-23	Fonctions utiles	herbelin
2003-09-23	Utilisation de noms dans 'Implicit Arguments [...]'	herbelin
2003-09-21	Mise en place d'implicites par noms en v8	herbelin
2003-09-12	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-09	error	herbelin
2003-09-02	Export process_module_bindings pour traducteur	herbelin
2003-08-11	Nouvelle mouture du traducteur v7->v8	herbelin
2003-06-10	Passage des noms de tactiques à kernel_name pour compatibilité avec les fon...	herbelin
2003-06-10	Déplacement traducteur de nom dans Constrextern pour accès aux noms longs	herbelin
2003-06-10	code mort	herbelin
2003-05-20	Extension renommage	herbelin