aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* On laisse les LetIn dans les types des constructeurs et des éliminationsGravatar herbelin2000-09-15
* CommentairesGravatar herbelin2000-09-15
* Messages d'erreursGravatar herbelin2000-09-15
* Expression anglaiseGravatar herbelin2000-09-15
* Minor correction for Ocamlweb + doc updateGravatar coq2000-09-14
* Bugs parenthèsesGravatar herbelin2000-09-14
* MAJGravatar herbelin2000-09-14
* Suppression Redinfo Sosub AbstractionGravatar herbelin2000-09-14
* Abstraction de constrGravatar herbelin2000-09-14
* Déplacement de fonctions de Reduction vers TacredGravatar herbelin2000-09-14
* Nouvelle version de frterm; ajout des contextes dans l'enviornnement de rédu...Gravatar herbelin2000-09-14
* Intégré à TacredGravatar herbelin2000-09-14
* Rendus obsolètes par le LetInGravatar herbelin2000-09-14
* Abstraction de constrGravatar herbelin2000-09-14
* MAJGravatar herbelin2000-09-12
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Vers la paramétrisation des fonctions de Reduction et vers la fusion deGravatar herbelin2000-09-12
* nettoyageGravatar herbelin2000-09-10
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract...Gravatar herbelin2000-09-10
* Uniformisation AddPath, Print LoadPath, ... en Add Path, Print PathGravatar herbelin2000-09-10
* Intégration à TermGravatar herbelin2000-09-10
* Canonisation de certains noms dans Pretyping, Asterm et Safe_typingGravatar herbelin2000-09-06
* code mortGravatar herbelin2000-09-06
* Ajout erreur unexpected typeGravatar herbelin2000-09-06
* kernel/type_errors.mlGravatar herbelin2000-09-06
* cosmétiqueGravatar herbelin2000-08-28
* Nametab.init - bug correctedGravatar coq2000-08-21
* Bug dans le filtrage des paires, nettoyageGravatar herbelin2000-08-20
* Pattern matching de sous-termesGravatar delahaye2000-08-17
* Pattern matching de sous-termes + exceptions dans le lexerGravatar delahaye2000-08-17
* reparation bug des coercions (cas ou on importe une coercion faisantGravatar barras2000-08-08
* messages d'erreurGravatar herbelin2000-07-28
* Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...Gravatar herbelin2000-07-28
* Ajout syntaxe [ phr1 ... phrn ]. pour grouper des commandes (pour Time ou Gra...Gravatar herbelin2000-07-26
* bug token "<:" et ":<"Gravatar herbelin2000-07-26
* dvips -o ==> dvips -o $@Gravatar coq2000-07-26
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
* MAJGravatar herbelin2000-07-24
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Passage à des contextes de vars et de rels pouvant contenir des déclaration...Gravatar herbelin2000-07-24
* *) -> i*)Gravatar filliatr2000-07-21
* retablissement minicoq (pour Jacek)Gravatar filliatr2000-07-21
* Pattern -> parsingGravatar delahaye2000-07-21
* Fail n + appel de interpGravatar delahaye2000-07-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 07:32:17 +0000