aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-10-08Renommage no-strict en -strict-implicitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4541 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Renommage no-strict en -strict-implicit; option -dont-load-proofsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4540 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Mise en place d'un mecanisme ne chargeant pas les preuves opaquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4539 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4538 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Essai de traduction du contraire de 'tacledit bin/coqtop.byte' en 'tac...'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4537 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Debranchement de l'affichage automatique de Proof par le traducteur (trop ↵herbelin
complique de trouver la bonne indentation); affichage en revanche de Proof s'il existait deja git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4536 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Inspect saute maintenant les marqueurs invisiblesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4535 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Compatibilite V7 des noms d'hypothesesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4533 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-06Pour rendre make un peu moins verbeuxletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4532 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-06NEWCONTRIBVO doit apparaitre apres CONTRIBVOherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4531 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-06pour ocamlwebletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4530 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-06distinguer interp_cs et interp_setcsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4529 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-04Debranchement de la regle .v.vo pour que celle-ci ne soit pas prise quand ↵herbelin
newtheories et newcontrib n'existent pas encore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4528 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-04Reparation plus juste de l'inefficacite avec loaded_modules (respecte l'ordre)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4527 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-04NEW*VO doit apparaitre apres *VO + diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4526 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-04majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4525 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-03pr_vernac est paresseux; States.unfreeze seulement après que msgnl aitherbelin
dégelé pr_vernac; hack pour "Import nat_scope" and co. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4524 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-03Bug cible newtheories/Init + diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4523 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-03Cacher les .v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4522 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-03Correction bug explosion de la taille de la liste loaded_modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4521 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-03Nettoyage, simplification et compatibilite -jherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4520 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-03oubli de deux flags -v7letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4519 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-03*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4518 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-02Pas de renommage des noms de sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4517 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-02as au niveau de appherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4516 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-02Hypothesis mot-cleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4515 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-02Traduction des tests success et test en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4514 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-02Plus de nom commencant par '_' en V8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4513 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-02Le nom '_' n'est plus valable en v8 pour nommer les variablesherbelin
dépendantes qui par hasard aurait été déclarées Anonymous git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4512 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-01Retour sur la version non optimisee de 'add' pour compatibilite; renommage ↵herbelin
Un_suivi_de et Zero_suivi_de; nouveaux resultats sur 'times' et 'entier' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4511 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-01cosmetiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4510 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-01Implantation de l'option 'format' des Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4509 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4508 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30'_ = _ = _' maintenant predefini, meme en V7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4507 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30Ajout 'Close Scope', mise en place de la structure pour un modificateur 'format'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4506 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30Les notations hors scope s'empilent maintenant comme des scopes neherbelin
contenant qu'une notation + renommage dans Reals git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4505 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4504 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30Les notations hors scope s'empilent maintenant comme des scopes neherbelin
contenant qu'une notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4503 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30Ajout 'Close Scope'.herbelin
Mise en place de la structure pour un modificateur 'format' de Notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4502 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30Ajout 'Close Scope'.herbelin
Les notations hors scope s'empilent maintenant comme des scopes ne contenant qu'une notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4501 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30Ajout 'Close Scope'.herbelin
Les notations hors scope s'empilent maintenant comme des scopes ne contenant qu'une notation. Mise en place de la structure pour un modificateur 'format' de Notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4500 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-29Oubli du type du terme a filtrer quand pas d'argument dans la traduction de caseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4499 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-29Prise en compte d'un inductif sans argument dans le 'in' des 'match'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4498 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-28oupsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4497 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-282 pbs de plus réglés concernant Setoid Ring:letouzey
- pf_conv_x parfois utilisé sur des termes non typés -> un try with - setoid_replace peut parfois résoudre seul l'égalité utilisé -> un tclTRY git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4496 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-28une induction de moins dans lt_eq_lt_decletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4495 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-28well_founded_induction de nouveau transparentletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4494 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4493 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Bug aboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4492 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-18 17:59:34 +0000