aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Intégration à TermGravatar herbelin2000-09-10
* Canonisation de certains noms dans Pretyping, Asterm et Safe_typingGravatar herbelin2000-09-06
* Ajout erreur unexpected typeGravatar herbelin2000-09-06
* kernel/type_errors.mlGravatar herbelin2000-09-06
* Pattern matching de sous-termesGravatar delahaye2000-08-17
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* retablissement minicoq (pour Jacek)Gravatar filliatr2000-07-21
* Quelques (*i*) pour ne pas casser oczmlwebGravatar coq2000-07-19
* Plus de env et sigma dans get_arity, plus de sigma dans make_arityGravatar herbelin2000-07-01
* Précalcul de la forme canonique des constructeurs et arités pour traiter le...Gravatar herbelin2000-07-01
* Ajout fonctions sur les aritésGravatar herbelin2000-07-01
* Précalcul de la forme canonique des constructeurs et arités pour traiter le...Gravatar herbelin2000-07-01
* Extension de find_inductive aux co-inductifs et renommage en find_rectypeGravatar herbelin2000-07-01
* Relative prend sigma en plus pour la normalisation du message d'erreurGravatar herbelin2000-06-29
* BroutillesGravatar herbelin2000-06-29
* Ajout make_typed_lazyGravatar herbelin2000-06-29
* Normalisation des Evar avant génération des erreursGravatar herbelin2000-06-29
* bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...Gravatar filliatr2000-06-21
* DocGravatar herbelin2000-06-09
* DiversGravatar herbelin2000-06-03
* Retrait des lam_and_pop and co; ajout d'un destructeur 'lispien' de constrGravatar herbelin2000-06-03
* Retrait de decomp_prod non conforme à sa specGravatar herbelin2000-06-02
* Retrait de certains castsGravatar herbelin2000-06-02
* docGravatar herbelin2000-06-02
* Bug DLAM dans strongGravatar herbelin2000-06-02
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de GenericGravatar herbelin2000-05-31
* Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursGravatar herbelin2000-05-31
* Modification messages d'erreurs, possibilité de n'importe quel constr dans l...Gravatar herbelin2000-05-26
* Bug existential_value au lieu de existential_type + divers sur existentialGravatar herbelin2000-05-25
* CommentairesGravatar herbelin2000-05-22
* Renommage hypothèses de nom redondant dans les environnementsGravatar herbelin2000-05-22
* suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsGravatar herbelin2000-05-22
* Changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* MAJ modifs InductiveGravatar herbelin2000-05-18
* Ajouts des causes d'erreur de IndrecGravatar herbelin2000-05-18
* Restructuration des outils pour les inductifs.Gravatar herbelin2000-05-18
* Ajout lift_contextGravatar herbelin2000-05-18
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* Centralisation prod_name and co dans Environ; mkLambda_string dans TermGravatar herbelin2000-05-18
* Restructuration des outils pour les inductifs.Gravatar herbelin2000-05-18
* Centralisation prod_name and co dans Environ; mkLambda_string dans TermGravatar herbelin2000-05-18
* Ajout mis_typepathGravatar herbelin2000-05-16
* docGravatar herbelin2000-05-05
* Ajout d'un strong 'light'Gravatar herbelin2000-05-05
* Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)Gravatar herbelin2000-05-04
* Retrait de PrintConstr vers top_printersGravatar delahaye2000-05-03
* diverses modifs pour ocamlwebGravatar filliatr2000-05-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 17:45:35 +0000