aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-05-11m.a.j. PROBLEMES/TODOletouzey
2001-05-11construct_reference regarde d'abord dans le contexte local, puis les globauxfilliatr
2001-05-10exemples Magicletouzey
2001-05-10message 'is defined' seulement en mode verbosefilliatr
2001-05-10retouche de extract_inductive_declarationletouzey
2001-05-10ajout d'un afficher de contexte et d'une fonction constbody_of_stringletouzey
2001-05-10Bug lift de la contrainte au passage du let (bug rapporte par S. Boulme)herbelin
2001-05-09nettoyage extractionfilliatr
2001-05-09cleanup + comments, toujoursletouzey
2001-05-07ex d'utilisation de fourier avec fieldmayero
2001-05-07integration de field a fouriermayero
2001-05-07quelques bug reports mineursbarras
2001-05-04commentairesletouzey
2001-05-03Changement de la structure des points fixesbarras
2001-05-02commentaires sur renommages des var dans extract_typeletouzey
2001-04-30cleanup, commentsletouzey
2001-04-30ocamlwebfilliatr
2001-04-30commentaires mlutil + binders_fold en coursletouzey
2001-04-25ajout pour le cdrommayero
2001-04-25Notes pour la version Windowsdelahaye
2001-04-25*** empty log message ***courant
2001-04-25*** empty log message ***courant
2001-04-25*** empty log message ***courant
2001-04-25ligne vide lors de l'affichage des messages d'erreur a toplevel entrebarras
2001-04-25message d'erreur pour rattrapper l'anomalie avec SQUASHbarras
2001-04-25make -j world -> make world en raison de bug ocamlc/ocamloptcourant
2001-04-25man pages for coq-interface and parsercourant
2001-04-25Ajout pages de man coq_makefile et coqmktopcourant
2001-04-25modif pour RPM et Debiancourant
2001-04-25modif rpmcourant
2001-04-25make reals prend en compte tous les .vo de theories/Realsfilliatr
2001-04-25coqwebfilliatr
2001-04-25- Ajout pages de man pour coqc, coqtop, coqtop.opt et coqtop.bytecourant
2001-04-25Amelioration message args constructeurherbelin
2001-04-25Bug perte d'alias avec type dependentsherbelin
2001-04-25Amelioration affichageherbelin
2001-04-25MAJherbelin
2001-04-25MAJherbelin
2001-04-24SearchIsos n'a pas encore ete portedelahaye
2001-04-24Messages d'erreur Casesherbelin
2001-04-24correction nommayero
2001-04-24Les clauses de Rec doivent prendre des tactic_atom'sdelahaye
2001-04-24Suppression d'une partie de code commentedelahaye
2001-04-24Ajout du cas True->A|-Bdelahaye
2001-04-24interdiction occ positives ET negatives dans Patternwerner
2001-04-24Reorganisation pour Ltacdelahaye
2001-04-24Mise a jour V7mohring
2001-04-24README avec ref (2)letouzey
2001-04-24TODO in v.o., test/Makefile moins pire, README avec refletouzey
2001-04-24Ajout du .dependmohring