aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilite V7 des noms d'hypothesesGravatar herbelin2003-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4533 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour rendre make un peu moins verbeuxGravatar letouzey2003-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4532 85f007b7-540e-0410-9357-904b9bb8a0f7
* NEWCONTRIBVO doit apparaitre apres CONTRIBVOGravatar herbelin2003-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4531 85f007b7-540e-0410-9357-904b9bb8a0f7
* pour ocamlwebGravatar letouzey2003-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4530 85f007b7-540e-0410-9357-904b9bb8a0f7
* distinguer interp_cs et interp_setcsGravatar letouzey2003-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4529 85f007b7-540e-0410-9357-904b9bb8a0f7
* Debranchement de la regle .v.vo pour que celle-ci ne soit pas prise quand ↵Gravatar herbelin2003-10-04
| | | | | | 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
* Reparation plus juste de l'inefficacite avec loaded_modules (respecte l'ordre)Gravatar herbelin2003-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4527 85f007b7-540e-0410-9357-904b9bb8a0f7
* NEW*VO doit apparaitre apres *VO + diversGravatar herbelin2003-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4526 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4525 85f007b7-540e-0410-9357-904b9bb8a0f7
* pr_vernac est paresseux; States.unfreeze seulement après que msgnl aitGravatar herbelin2003-10-03
| | | | | | | 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
* Bug cible newtheories/Init + diversGravatar herbelin2003-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4523 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cacher les .v8Gravatar herbelin2003-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4522 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug explosion de la taille de la liste loaded_modulesGravatar herbelin2003-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4521 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage, simplification et compatibilite -jGravatar herbelin2003-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4520 85f007b7-540e-0410-9357-904b9bb8a0f7
* oubli de deux flags -v7Gravatar letouzey2003-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4519 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4518 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pas de renommage des noms de sectionGravatar herbelin2003-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4517 85f007b7-540e-0410-9357-904b9bb8a0f7
* as au niveau de appGravatar herbelin2003-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4516 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hypothesis mot-cleGravatar herbelin2003-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4515 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction des tests success et test en v8Gravatar herbelin2003-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4514 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de nom commencant par '_' en V8Gravatar herbelin2003-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4513 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le nom '_' n'est plus valable en v8 pour nommer les variablesGravatar herbelin2003-10-02
| | | | | | | 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
* Retour sur la version non optimisee de 'add' pour compatibilite; renommage ↵Gravatar herbelin2003-10-01
| | | | | | 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
* cosmetiqueGravatar herbelin2003-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4510 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implantation de l'option 'format' des NotationsGravatar herbelin2003-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4509 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4508 85f007b7-540e-0410-9357-904b9bb8a0f7
* '_ = _ = _' maintenant predefini, meme en V7Gravatar herbelin2003-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4507 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'Close Scope', mise en place de la structure pour un modificateur 'format'Gravatar herbelin2003-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4506 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les notations hors scope s'empilent maintenant comme des scopes neGravatar herbelin2003-09-30
| | | | | | | 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
* code mortGravatar herbelin2003-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4504 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les notations hors scope s'empilent maintenant comme des scopes neGravatar herbelin2003-09-30
| | | | | | | contenant qu'une notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4503 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'Close Scope'.Gravatar herbelin2003-09-30
| | | | | | | 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
* Ajout 'Close Scope'.Gravatar herbelin2003-09-30
| | | | | | | | 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
* Ajout 'Close Scope'.Gravatar herbelin2003-09-30
| | | | | | | | | 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
* Oubli du type du terme a filtrer quand pas d'argument dans la traduction de caseGravatar herbelin2003-09-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4499 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte d'un inductif sans argument dans le 'in' des 'match'Gravatar herbelin2003-09-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4498 85f007b7-540e-0410-9357-904b9bb8a0f7
* oupsGravatar letouzey2003-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4497 85f007b7-540e-0410-9357-904b9bb8a0f7
* 2 pbs de plus réglés concernant Setoid Ring:Gravatar letouzey2003-09-28
| | | | | | | | - 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
* une induction de moins dans lt_eq_lt_decGravatar letouzey2003-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4495 85f007b7-540e-0410-9357-904b9bb8a0f7
* well_founded_induction de nouveau transparentGravatar letouzey2003-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4494 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4493 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug aboutGravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4492 85f007b7-540e-0410-9357-904b9bb8a0f7
* Syntaxe plus liberale pour le type des arguments de filtrage du 'match'Gravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4491 85f007b7-540e-0410-9357-904b9bb8a0f7
* Syntaxe plus liberale pour le type des arguments de filtrage du 'match'; ↵Gravatar herbelin2003-09-26
| | | | | | traduction de noms git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4490 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4489 85f007b7-540e-0410-9357-904b9bb8a0f7
* pa_ifdef.cmo redondantGravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4488 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout now_showGravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4487 85f007b7-540e-0410-9357-904b9bb8a0f7
* About, InfixGravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4486 85f007b7-540e-0410-9357-904b9bb8a0f7
* 'Open Local Scope' en attendant que le core_scope sache se mettre devant ↵Gravatar herbelin2003-09-26
| | | | | | implicitement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4485 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-04 05:28:13 +0000