aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2000-10-27Intro choue si le nom d'hypothse existe au lieu de mettre un avertissementherbelin
2000-10-27Ajoute : Ast dans la regle de grammairemayero
2000-10-27g_natsyntax et g_zsyntax maintenant toujours linkesfilliatr
2000-10-27Mise a jour TheoryListmohring
2000-10-26MAJherbelin
2000-10-26Essai de remplacement du whd_betaiotaevar de Qed par un whd_iseherbelin
2000-10-26Suppression cas Cast dans whd_ise et whd_ise1; Suppression du cast au moment ...herbelin
2000-10-26Require Export recursifsfilliatr
2000-10-26Semi_Ring_Theory_of decommentemohring
2000-10-26Retire les parentheses autour des tactiquesmohring
2000-10-26Ajout de la mthode load_function pour exporter les 'tactic-ring-theory'herbelin
2000-10-26Bug Simpl avec Cases cache sous plusieurs constantesherbelin
2000-10-26Renommage var en named et decl en assumherbelin
2000-10-26ntrefiner.ml* removed in module xmlsacerdot
2000-10-25Manquait le cas Constr de dyn_polynomherbelin
2000-10-25Bug pop_path_prefix : List.rev manquantherbelin
2000-10-25Porting from V6 finished, but not working.sacerdot
2000-10-25Added xml contribution to configuresacerdot
2000-10-25xml contribution added to the Makefilesacerdot
2000-10-25xml contribution created.sacerdot
2000-10-24MAJherbelin
2000-10-24Changement des analyseurs syntaxiques de Grammar et Syntaxherbelin
2000-10-24un espaceherbelin
2000-10-24Syntaxe des tactiquesherbelin
2000-10-24Renommage command -> constr et changement des analyseurs syntaxiques de Gramm...herbelin
2000-10-24Bug réduction suite modifs let-inherbelin
2000-10-24Meilleur endroit pour déclarer les parseurs de grammaires et joli affichageherbelin
2000-10-24Bug de copier-collerherbelin
2000-10-23MAJherbelin
2000-10-23Modifications pour implicites améliorésherbelin
2000-10-23Rétablissement compatibilité des implicites (2ème) (mais amélioration)herbelin
2000-10-23MAJherbelin
2000-10-23Import de Infix au Requireherbelin
2000-10-23code mortherbelin
2000-10-23MAJherbelin
2000-10-23L'état implicite des définitions survivant au discharge redevient celui du ...herbelin
2000-10-23module_segment et module_filenamefilliatr
2000-10-23La réduction du Let s'appelle maintenant zeta comme dans le lambda-mu-calculherbelin
2000-10-23Simplifications/questionsherbelin
2000-10-23MAJherbelin
2000-10-23Petit nettoyage de Evarutil et Evarconvherbelin
2000-10-21Bug indices dans l'instance d'une evarherbelin
2000-10-21Pb affichage warningherbelin
2000-10-19Nettoyage Coercionherbelin
2000-10-19MAJherbelin
2000-10-19Use UTF-8 as default encoding for computing length of strings in prettymiquel
2000-10-18MAJherbelin
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-18docherbelin