aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-09-23Utilisation de noms dans 'Implicit Arguments [...]'herbelin
2003-09-23Changement de l'afficheur pour que les variables liées aient un nom indépen...herbelin
2003-09-23Ajout fonctions syntaxe v8 pour contrib MapleModeherbelin
2003-09-23Correction bug 328coq
2003-09-23test d'implicite incorrect depuis que eq porte sur Typebarras
2003-09-23Bug internalisation des Extern: la globalisation doit etre stricteherbelin
2003-09-23majfilliatr
2003-09-22commit accidentel d'une bidouilleletouzey
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
2003-09-22L'exemple phare de modules - simplifie pour TPHOLscoq
2003-09-22MAJherbelin
2003-09-22Anglaisherbelin
2003-09-22Système de renommage des noms de tactiques Ltacherbelin
2003-09-22Bug d'externalisation des constantes avec uniquement des implicitesherbelin
2003-09-22suite (et fin) reparation Setoid Ringletouzey
2003-09-22typo (Benjamin, voyons ;)letouzey
2003-09-22Distfix aussi adopte le nouveau schema de V8onlyherbelin
2003-09-22Implicits maintenant au courant pour l'affichageherbelin
2003-09-22Deplacement de lemmes de IntMap vers ZArithherbelin
2003-09-22tentative de rafraichissement de Setoid Ringletouzey
2003-09-22message d'erreur de garde des cofixbarras
2003-09-22Passage à la V8 par défautherbelin
2003-09-21Renommage Implicits -> Implicitherbelin
2003-09-21Mise en place d'implicites par noms en v8herbelin
2003-09-21Renommages divers.herbelin
2003-09-21Changement de la politique de V8only: V8only tout seul signifieherbelin
2003-09-21Parsing au niveau lconstr des patterns de 'match context'herbelin
2003-09-21Changement de la politique de V8only: V8only tout seul signifieherbelin
2003-09-21Mise en place d'implicites par noms en v8herbelin
2003-09-21Conflit de nom Pplus dans positive et dans polynomial (de ring)herbelin
2003-09-21Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...herbelin
2003-09-21Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...herbelin
2003-09-21Nettoyageherbelin
2003-09-19coqide auto complete initial bug fixmarche
2003-09-19Coqide : les nouveaute d'aoutmonate
2003-09-19'::' est deja pris en V7herbelin
2003-09-19majfilliatr
2003-09-19Section et report Infix hors sectionherbelin
2003-09-19Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le tr...herbelin
2003-09-19Mise en place des V8Notation et V8Infix pour déclarer des notations enherbelin
2003-09-19Ajout notation :: pour consherbelin
2003-09-19Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...herbelin
2003-09-19parsingherbelin
2003-09-18Interface Eautoherbelin
2003-09-18Traduction de Instantiateherbelin
2003-09-18Niveau du 'as' des motifsherbelin
2003-09-18Traduction de '_' comme referenceherbelin
2003-09-18Parsing correct des explicites en cas de projectionherbelin
2003-09-18Plutôt que de faire "Load" silencieusement, en profiter pour traduireherbelin
2003-09-18Ajout r gle d'affichage tactiques èéfinies par Notationherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-22 05:29:05 +0000