coq - The formal proof system

Age	Commit message (Expand)	Author
2003-10-13	Deplacement pr_subgoal and co vers Pfedit	herbelin
2003-10-13	Ajout d'une fonction de recherche sur les composantes du nom des objets	herbelin
2003-10-13	Protection contre les noms de lemmes existant deja	herbelin
2003-10-13	Deplacement pr_subgoal and co vers Pfedit; Ajout SearchNamed	herbelin
2003-10-11	translate_file etait abusivement positionne	herbelin
2003-10-10	changement nouvelle syntaxe (pt fixes)	barras
2003-10-10	Renommage en v8 de PolyList en List et List en MonoList	herbelin
2003-10-09	Nouveau format de l'option 'format'	herbelin
2003-10-08	Prise en compte des paramètres implicites d'inductifs pour la globalisation ...	herbelin
2003-10-08	Des abbreviations pour constrintern.ml	herbelin
2003-10-08	Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...	herbelin
2003-10-08	Renommage no-strict en -strict-implicit; option -dont-load-proofs	herbelin
2003-10-07	Debranchement de l'affichage automatique de Proof par le traducteur (trop com...	herbelin
2003-10-07	Correction du bug 335 et Export/Require Export dans un module	coq
2003-10-04	Reparation plus juste de l'inefficacite avec loaded_modules (respecte l'ordre)	herbelin
2003-10-03	pr_vernac est paresseux; States.unfreeze seulement après que msgnl ait	herbelin
2003-10-03	Correction bug explosion de la taille de la liste loaded_modules	herbelin
2003-10-01	Implantation de l'option 'format' des Notations	herbelin
2003-09-30	Ajout 'Close Scope'.	herbelin
2003-09-30	Ajout 'Close Scope'.	herbelin
2003-09-26	Ajout 'About'	herbelin
2003-09-26	Decouplage printing en v8 pour les interpretations de notations	herbelin
2003-09-25	V8Infix declarait a tort une regle d'interpretation V7	herbelin
2003-09-24	Traduction aussi si -translate et -load-vernac-source	herbelin
2003-09-23	Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...	herbelin
2003-09-23	Utilisation de noms dans 'Implicit Arguments [...]'	herbelin
2003-09-22	traducteur: affiche les commentaires a l'interieur des commandes	barras
2003-09-22	Anglais	herbelin
2003-09-22	message d'erreur de garde des cofix	barras
2003-09-21	Renommage Implicits -> Implicit	herbelin
2003-09-21	Changement de la politique de V8only: V8only tout seul signifie	herbelin
2003-09-19	parsing	herbelin
2003-09-18	Plutôt que de faire "Load" silencieusement, en profiter pour traduire	herbelin
2003-09-18	Ajout r gle d'affichage tactiques èéfinies par Notation	herbelin
2003-09-16	Pour cacher le contenu de Load au traducteur	herbelin
2003-09-16	Tentative amelioration pretty-printing symboles	herbelin
2003-09-16	(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)...	herbelin
2003-09-16	(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)	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 d'un morceau de Declare	herbelin
2003-09-12	Ajout 'Print Scopes' et 'Bind Scope with classes'	herbelin
2003-09-12	Déplacement de Declare et déclarations des scopes d'argument dans Declare	herbelin
2003-09-10	Debranchement du traducteur pour Load !	herbelin
2003-09-10	Traduction de Distfix	herbelin
2003-09-06	Mise en place possibilité de définitions locales dans les paramètres des r...	herbelin
2003-09-06	Paramétrisation vis à vis de existential_key	herbelin
2003-09-06	Mise en place possibilité de définitions locales dans les paramètres des i...	herbelin
2003-09-02	Freeze mal place	herbelin
2003-08-31	Mise en oeuvre de la syntaxe des inductifs a la ML 'Inductive nat : Set := O ...	herbelin
2003-08-14	Fusion -translate et -ftranslate	herbelin