aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2000-09-26MAJherbelin
2000-09-18mise a jour dependancesfilliatr
2000-09-15On laisse les LetIn dans les types des constructeurs et des éliminationsherbelin
2000-09-15Commentairesherbelin
2000-09-15Messages d'erreursherbelin
2000-09-15Expression anglaiseherbelin
2000-09-14Minor correction for Ocamlweb + doc updatecoq
2000-09-14Bugs parenthèsesherbelin
2000-09-14MAJherbelin
2000-09-14Suppression Redinfo Sosub Abstractionherbelin
2000-09-14Abstraction de constrherbelin
2000-09-14Déplacement de fonctions de Reduction vers Tacredherbelin
2000-09-14Nouvelle version de frterm; ajout des contextes dans l'enviornnement de rédu...herbelin
2000-09-14Intégré à Tacredherbelin
2000-09-14Rendus obsolètes par le LetInherbelin
2000-09-14Abstraction de constrherbelin
2000-09-12MAJherbelin
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
2000-09-12Vers la paramétrisation des fonctions de Reduction et vers la fusion deherbelin
2000-09-10nettoyageherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Suppression de Abstherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-09-10Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract...herbelin
2000-09-10Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Pathherbelin
2000-09-10Intégration à Termherbelin
2000-09-06Canonisation de certains noms dans Pretyping, Asterm et Safe_typingherbelin
2000-09-06code mortherbelin
2000-09-06Ajout erreur unexpected typeherbelin
2000-09-06kernel/type_errors.mlherbelin
2000-08-28cosmétiqueherbelin
2000-08-21Nametab.init - bug correctedcoq
2000-08-20Bug dans le filtrage des paires, nettoyageherbelin
2000-08-17Pattern matching de sous-termesdelahaye
2000-08-17Pattern matching de sous-termes + exceptions dans le lexerdelahaye
2000-08-08reparation bug des coercions (cas ou on importe une coercion faisantbarras
2000-07-28messages d'erreurherbelin
2000-07-28Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...herbelin
2000-07-26Ajout syntaxe [ phr1 ... phrn ]. pour grouper des commandes (pour Time ou Gra...herbelin
2000-07-26bug token "<:" et ":<"herbelin
2000-07-26dvips -o ==> dvips -o $@coq
2000-07-25retablissement make doc et make minicoqfilliatr
2000-07-24MAJherbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclaration...herbelin
2000-07-21*) -> i*)filliatr
2000-07-21retablissement minicoq (pour Jacek)filliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 06:47:50 +0000