aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-10-08Renommage no-strict en -strict-implicitherbelin
2003-10-08Renommage no-strict en -strict-implicit; option -dont-load-proofsherbelin
2003-10-08Mise en place d'un mecanisme ne chargeant pas les preuves opaquesherbelin
2003-10-07majfilliatr
2003-10-07Essai de traduction du contraire de 'tacledit bin/coqtop.byte' en 'tac...'herbelin
2003-10-07Debranchement de l'affichage automatique de Proof par le traducteur (trop com...herbelin
2003-10-07Inspect saute maintenant les marqueurs invisiblesherbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-10-07Compatibilite V7 des noms d'hypothesesherbelin
2003-10-06Pour rendre make un peu moins verbeuxletouzey
2003-10-06NEWCONTRIBVO doit apparaitre apres CONTRIBVOherbelin
2003-10-06pour ocamlwebletouzey
2003-10-06distinguer interp_cs et interp_setcsletouzey
2003-10-04Debranchement de la regle .v.vo pour que celle-ci ne soit pas prise quand new...herbelin
2003-10-04Reparation plus juste de l'inefficacite avec loaded_modules (respecte l'ordre)herbelin
2003-10-04NEW*VO doit apparaitre apres *VO + diversherbelin
2003-10-04majfilliatr
2003-10-03pr_vernac est paresseux; States.unfreeze seulement après que msgnl aitherbelin
2003-10-03Bug cible newtheories/Init + diversherbelin
2003-10-03Cacher les .v8herbelin
2003-10-03Correction bug explosion de la taille de la liste loaded_modulesherbelin
2003-10-03Nettoyage, simplification et compatibilite -jherbelin
2003-10-03oubli de deux flags -v7letouzey
2003-10-03*** empty log message ***barras
2003-10-02Pas de renommage des noms de sectionherbelin
2003-10-02as au niveau de appherbelin
2003-10-02Hypothesis mot-cleherbelin
2003-10-02Traduction des tests success et test en v8herbelin
2003-10-02Plus de nom commencant par '_' en V8herbelin
2003-10-02Le nom '_' n'est plus valable en v8 pour nommer les variablesherbelin
2003-10-01Retour sur la version non optimisee de 'add' pour compatibilite; renommage Un...herbelin
2003-10-01cosmetiqueherbelin
2003-10-01Implantation de l'option 'format' des Notationsherbelin
2003-10-01majfilliatr
2003-09-30'_ = _ = _' maintenant predefini, meme en V7herbelin
2003-09-30Ajout 'Close Scope', mise en place de la structure pour un modificateur 'format'herbelin
2003-09-30Les notations hors scope s'empilent maintenant comme des scopes neherbelin
2003-09-30code mortherbelin
2003-09-30Les notations hors scope s'empilent maintenant comme des scopes neherbelin
2003-09-30Ajout 'Close Scope'.herbelin
2003-09-30Ajout 'Close Scope'.herbelin
2003-09-30Ajout 'Close Scope'.herbelin
2003-09-29Oubli du type du terme a filtrer quand pas d'argument dans la traduction de caseherbelin
2003-09-29Prise en compte d'un inductif sans argument dans le 'in' des 'match'herbelin
2003-09-28oupsletouzey
2003-09-282 pbs de plus réglés concernant Setoid Ring:letouzey
2003-09-28une induction de moins dans lt_eq_lt_decletouzey
2003-09-28well_founded_induction de nouveau transparentletouzey
2003-09-27majfilliatr
2003-09-26Bug aboutherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 01:45:34 +0000