aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* documentationGravatar filliatr2000-01-28
* erreurs latex dans interfacesGravatar filliatr2000-01-27
* mise a jourGravatar filliatr2000-01-26
* lorsque ocamlc est donne a la main, alors ocamlopt est positionne avecGravatar filliatr2000-01-26
* MAJ ocaml 2.99 (espaces dans la syntaxe des cast)Gravatar herbelin2000-01-26
* Fin du changement comarg -> constrargGravatar herbelin2000-01-26
* MAJ commentairesGravatar herbelin2000-01-26
* Abstraction de l'implémentation des signatures de Sign en vue intégration d...Gravatar herbelin2000-01-26
* gros commit de tout ce que j'ai fait pendant les vacances :Gravatar filliatr2000-01-21
* Bête renommageGravatar herbelin2000-01-20
* BroutillesGravatar herbelin2000-01-20
* Nettoyage des fichiers de parsingGravatar herbelin2000-01-13
* Plus d'unfold inutile des Fix dans SimplGravatar herbelin2000-01-13
* Ajout de RecordGravatar herbelin2000-01-11
* BugsGravatar herbelin2000-01-11
* Ajout '|' en tete de filtrageGravatar herbelin2000-01-11
* Grammaire pour Grammar et Syntax, avant dans ExtendGravatar herbelin2000-01-07
* Traduction constr->rawconstr (avant dans TermastGravatar herbelin2000-01-07
* Restructuration printer et parserGravatar herbelin2000-01-07
* Restructuration diversesGravatar herbelin2000-01-07
* MAJGravatar herbelin2000-01-07
* Renommage command en constrGravatar herbelin2000-01-07
* Déplacement print_emacs dans OptionsGravatar herbelin2000-01-07
* Correction pbs liés aux evarGravatar herbelin2000-01-07
* Déplacement non-affichage des coercions dans termastGravatar herbelin2000-01-07
* Restructuration printer et parserGravatar herbelin2000-01-07
* Renommage command en constrGravatar herbelin2000-01-07
* erreurs de syntax :$Gravatar filliatr1999-12-16
* bug : import -> export dans RequireGravatar filliatr1999-12-16
* message erreur SchemeGravatar herbelin1999-12-15
* Bug liftGravatar herbelin1999-12-15
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* Les inductifs dans Scheme doivent être des ident d'inductifsGravatar herbelin1999-12-15
* clarification du codeGravatar filliatr1999-12-14
* rattrapage exceptions autres que UserErrorGravatar filliatr1999-12-14
* sauvegarde de la valeur de module_nameGravatar filliatr1999-12-14
* bug mk_clenv_from lorsque pas d argumentsGravatar filliatr1999-12-14
* pretty-printers pour le debuggerGravatar filliatr1999-12-14
* mise a jour de refiner.ml (reports de modifs de la V6.3)Gravatar barras1999-12-13
* - états fabriqués avec -silentGravatar filliatr1999-12-13
* - méthode load sur les HintsGravatar filliatr1999-12-13
* chemin compile des fichiers CoqGravatar filliatr1999-12-13
* petite erreur dans CommandGravatar filliatr1999-12-13
* documentationGravatar filliatr1999-12-13
* documentation interfacesGravatar filliatr1999-12-13
* fichiers prelude CoqGravatar filliatr1999-12-13
* Poursuite intégration du CasesGravatar herbelin1999-12-13
* Ajout pp pattern et rawtermGravatar herbelin1999-12-12
* mise a jourGravatar filliatr1999-12-12
* modules et coqcGravatar filliatr1999-12-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 20:07:01 +0000