aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2003-09-18Simplification afficheur de tactiques non primitiveherbelin
2003-09-18bug fix: term reduced in bad envbarras
2003-09-17majfilliatr
2003-09-16En attendant l'afficheur...herbelin
2003-09-16Pour appliquer les noms reserves aussi aux bindersherbelin
2003-09-16Pour cacher le contenu de Load au traducteurherbelin
2003-09-16Tentative amelioration pretty-printing symbolesherbelin
2003-09-16(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 10:16:53 +0000