aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/printer.ml
Commit message (Expand)AuthorAge
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* Évaluation forcée des objets mis dans les streamsGravatar herbelin2000-12-14
* On force l'évaluation du qualid_of_global qui peut échouer dans le débuggerGravatar herbelin2000-12-14
* section_path etait en fait bonne dans ast et buggee dans printer.mlGravatar herbelin2000-12-06
* uniformisation messages d'erreurGravatar filliatr2000-11-27
* Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_spGravatar herbelin2000-11-23
* Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp;Gravatar herbelin2000-11-23
* Ajout pr_global_reference et is_visibleGravatar herbelin2000-11-20
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Suite du précédentGravatar herbelin2000-10-11
* Plus d'échec sur les globaux lorsque prterm est appelé par le débuggerGravatar herbelin2000-10-10
* Ajout de globpr dans tacprGravatar herbelin2000-10-03
* Disparition du type oper mais nouveau type global_referenceGravatar herbelin2000-10-01
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Modification messages d'erreurs, possibilité de n'importe quel constr dans l...Gravatar herbelin2000-05-26
* Réparation bug d'affichage et affichage des instanciations par des {...}Gravatar herbelin2000-05-23
* Suite intégration de constr_patternGravatar herbelin2000-04-30
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
* Introduction d'un type constr_pattern pour les différents filtragesGravatar herbelin2000-04-26
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Export gentermpr avec renommageGravatar herbelin2000-01-31
* Abstraction de l'implémentation des signatures de Sign en vue intégration d...Gravatar herbelin2000-01-26
* Restructuration printer et parserGravatar herbelin2000-01-07
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* modules et coqcGravatar filliatr1999-12-12
* Suppression Rel de rawconstr et correction de bugs d'affichageGravatar herbelin1999-12-10
* Ajout des messages d'erreurs de CasesGravatar herbelin1999-12-09
* Ajout des fonctions prpattern et prrawtermGravatar herbelin1999-12-01
* printersGravatar filliatr1999-12-01
* module PrinterGravatar filliatr1999-11-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 21:01:40 +0000