aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
* Ajout 'About'Gravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4484 85f007b7-540e-0410-9357-904b9bb8a0f7
* Induction -> NewInduction; '++' pour appGravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4483 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle serie de traductionsGravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4482 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-possibilite changement chaine infixe en passant v7 a v8Gravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4481 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage de Destruct a NewDestruct; '-' pour negbGravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4480 85f007b7-540e-0410-9357-904b9bb8a0f7
* Structuration de fast_integer en operations sur positive, proprietes des ↵Gravatar herbelin2003-09-26
| | | | | | operations sur positive, operations sur Z, proprietes des operations sur Z; suppression section; true_sub devient definition git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4479 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un peu plus de souplesse dans la globalisation des noms utilises par les ↵Gravatar herbelin2003-09-26
| | | | | | tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4478 85f007b7-540e-0410-9357-904b9bb8a0f7
* Decouplage printing en v8 pour les interpretations de notationsGravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4477 85f007b7-540e-0410-9357-904b9bb8a0f7
* Logic_TypeSyntax a disparuGravatar herbelin2003-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4476 85f007b7-540e-0410-9357-904b9bb8a0f7
* add_x_x de fast_integer vers auxiliaryGravatar herbelin2003-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4475 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retour provisoire a une sectionGravatar herbelin2003-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4474 85f007b7-540e-0410-9357-904b9bb8a0f7
* V8Infix declarait a tort une regle d'interpretation V7Gravatar herbelin2003-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4473 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage options via COQFLAGS plutot que OPTGravatar herbelin2003-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4472 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction aussi si -translate et -load-vernac-sourceGravatar herbelin2003-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4471 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression section, ce qui evite de repliquer les declarations d'InfixGravatar herbelin2003-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4470 85f007b7-540e-0410-9357-904b9bb8a0f7
* Destruct/Induction -> NewDestruct/NewInductionGravatar herbelin2003-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Destruct -> NewDestructGravatar herbelin2003-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4468 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de noms dans 'Implicit Arguments [...]'Gravatar herbelin2003-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4467 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4466 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de Induction/Destruct par NewInduction/NewDestructGravatar herbelin2003-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4465 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de Induction/Destruct par NewInduction/NewDestructGravatar herbelin2003-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4464 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-25 23:42:06 +0000