aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-09-25Retour provisoire a une sectionherbelin
2003-09-25V8Infix declarait a tort une regle d'interpretation V7herbelin
2003-09-24Passage options via COQFLAGS plutot que OPTherbelin
2003-09-24Traduction aussi si -translate et -load-vernac-sourceherbelin
2003-09-24Suppression section, ce qui evite de repliquer les declarations d'Infixherbelin
2003-09-24Destruct/Induction -> NewDestruct/NewInductionherbelin
2003-09-24Destruct -> NewDestructherbelin
2003-09-24Utilisation de noms dans 'Implicit Arguments [...]'herbelin
2003-09-24majfilliatr
2003-09-23Remplacement de Induction/Destruct par NewInduction/NewDestructherbelin
2003-09-23Remplacement de Induction/Destruct par NewInduction/NewDestructherbelin
2003-09-23Remplacement de Induction/Destruct par NewInduction/NewDestructherbelin
2003-09-23Correction bug NewInduction pour les inductifs de type 'ordinaux'herbelin
2003-09-23Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...herbelin
2003-09-23Fonctions utilesherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-08 22:36:22 +0000