aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
Commit message (Expand)AuthorAge
* bug Fix signalé par Alexandre (even/odd mal interprété)Gravatar filliatr2001-04-02
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationGravatar herbelin2001-03-11
* uniformisation avec constr des lieurs dans rawterm/patternGravatar herbelin2001-02-14
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* Bug vieux MatchGravatar herbelin2000-12-25
* Bug prédicat old Case/MatchGravatar herbelin2000-12-20
* Bugs calcul du prédicat des Cases et CaseGravatar herbelin2000-12-15
* Mise en pageGravatar herbelin2000-12-14
* Bugs prise en compte du prédicat dans le Cases; le prédicat du Cases devien...Gravatar herbelin2000-12-14
* Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypageGravatar herbelin2000-11-29
* resolution implicites dans produits (bug)Gravatar filliatr2000-11-24
* Utilisation de global_reference dans rawconstrGravatar herbelin2000-11-20
* Insertion de coercion au milieu des applications partielles et propagation de...Gravatar herbelin2000-11-08
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Petit nettoyage de Evarutil et EvarconvGravatar herbelin2000-10-23
* Nettoyage CoercionGravatar herbelin2000-10-19
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Suppression d'un test inutile dans RCastGravatar herbelin2000-10-13
* Prise en compte de Let dans build_dependent_inductiveGravatar herbelin2000-10-11
* Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...Gravatar herbelin2000-09-26
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Canonisation de certains noms dans Pretyping, Asterm et Safe_typingGravatar herbelin2000-09-06
* kernel/type_errors.mlGravatar herbelin2000-09-06
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Modifs d'interpretation de patternsGravatar delahaye2000-07-21
* portage RefineGravatar filliatr2000-07-20
* Plus de env et sigma dans get_arity, plus de sigma dans make_arityGravatar herbelin2000-07-01
* Extension de find_inductive aux co-inductifs et renommage en find_rectypeGravatar herbelin2000-07-01
* Achèvement abstraction du mécanisme (optionnel) de castGravatar herbelin2000-06-29
* Bugs et simplifications coercionsGravatar herbelin2000-06-02
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Afficahge des locationsGravatar herbelin2000-05-31
* Nettoyage de GenericGravatar herbelin2000-05-31
* Modification messages d'erreurs, possibilité de n'importe quel constr dans l...Gravatar herbelin2000-05-26
* RienGravatar herbelin2000-05-22
* suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsGravatar herbelin2000-05-22
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* RéorganisationGravatar herbelin2000-05-05
* Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)Gravatar herbelin2000-05-04
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'Gravatar herbelin2000-05-02
* Changement de représentation du contexte des réf dans rawconstr et patternGravatar herbelin2000-04-28
* N'importe quel rawconstr maintenant dans le contexte d'une référenceGravatar herbelin2000-04-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 18:05:37 +0000