aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Bug environnementGravatar herbelin2001-01-11
* Rajout de la restriction de l'instance en cas d'unification de 2 variables ex...Gravatar herbelin2001-01-04
* Rattrapage d'erreur pour le Case + Eval Compute in pour DefinitionGravatar delahaye2001-01-03
* Bug de contextesGravatar herbelin2000-12-26
* DĂ©placement du type stack de Reduction vers Closure et utilisation pour accĂ...Gravatar herbelin2000-12-26
* Pattern sera mieux dans Pretyping; relâchement head_pattern_boundGravatar herbelin2000-12-26
* Un nom long pour les variables de section qui font classe ou coercion; réorg...Gravatar herbelin2000-12-25
* Bug vieux MatchGravatar herbelin2000-12-25
* Bug prédicatGravatar herbelin2000-12-25
* Bug prédicat old Case/MatchGravatar herbelin2000-12-20
* RĂ©tablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ind...Gravatar herbelin2000-12-20
* Export fonction testant si un inductive est un recordGravatar herbelin2000-12-19
* Amélioration message d'erreur mauvais prédicatGravatar herbelin2000-12-18
* Debut de nettoyage de SimplGravatar mohring2000-12-18
* Suppression du warning several default clausesGravatar herbelin2000-12-16
* Bug env vis Ă  vis du let inGravatar herbelin2000-12-15
* Bugs calcul du prédicat des Cases et CaseGravatar herbelin2000-12-15
* PrinterGravatar mohring2000-12-15
* Mauvais env donné à new_isevarGravatar herbelin2000-12-14
* Oubli test de correction Ă  l'instantiation des evarsGravatar herbelin2000-12-14
* Mise en pageGravatar herbelin2000-12-14
* LetIn dans SimplGravatar mohring2000-12-14
* Raffinement erreur Wrong PredicateGravatar herbelin2000-12-14
* Bugs prise en compte du prédicat dans le Cases; le prédicat du Cases devien...Gravatar herbelin2000-12-14
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Hint Unfold Local + commentairesGravatar mohring2000-12-12
* Debut de reparation de simplGravatar mohring2000-12-11
* Bug Cases en presence d'une absence de clauseGravatar herbelin2000-12-05
* Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypageGravatar herbelin2000-11-29
* La table de pré-évaluation des constantes ne doit pas persister au dischargeGravatar herbelin2000-11-27
* Utilisation de Let In pour les constantes locales, prise en compte des Let In...Gravatar herbelin2000-11-27
* Branchement du mécanisme d'instantiation des Evar en présence de définitio...Gravatar herbelin2000-11-27
* Prise en compte des let-in dans les fonctions de réduction pour les tactiquesGravatar herbelin2000-11-27
* Prise en compte de noms absolus dans la nametabGravatar herbelin2000-11-26
* Remplacement de certains sp_of_id par des locateGravatar herbelin2000-11-26
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* resolution implicites dans produits (bug)Gravatar filliatr2000-11-24
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* Mieux Ă  sa place dans toplevelGravatar herbelin2000-11-20
* Utilisation de global_reference dans rawconstrGravatar herbelin2000-11-20
* Utilisation de global_reference dans rawconstrGravatar herbelin2000-11-20
* Utilisation de global_reference dans rawconstr; blindage pour quand appelé d...Gravatar herbelin2000-11-20
* Ajout erreur GlobalNotFoundGravatar herbelin2000-11-20
* Cablage des syntactif defs avec la Nametab des objetsGravatar herbelin2000-11-20
* Tables des eval_constant devient une CstmapGravatar herbelin2000-11-20
* methode exportGravatar filliatr2000-11-15
* Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...Gravatar herbelin2000-11-10
* merge_locGravatar herbelin2000-11-08
* Insertion de coercion au milieu des applications partielles et propagation de...Gravatar herbelin2000-11-08