index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
printer.ml
Commit message (
Expand
)
Author
Age
...
*
Simplifications autour de typed_type (renommé types par analogie avec sorts)...
herbelin
2000-10-18
*
Renommage canonique :
herbelin
2000-10-18
*
Suite du précédent
herbelin
2000-10-11
*
Plus d'échec sur les globaux lorsque prterm est appelé par le débugger
herbelin
2000-10-10
*
Ajout de globpr dans tacpr
herbelin
2000-10-03
*
Disparition du type oper mais nouveau type global_reference
herbelin
2000-10-01
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
Mise en place d'un choix constr/typed_type en remplacement de certains Cast
herbelin
2000-06-01
*
Modification messages d'erreurs, possibilité de n'importe quel constr dans l...
herbelin
2000-05-26
*
Réparation bug d'affichage et affichage des instanciations par des {...}
herbelin
2000-05-23
*
Suite intégration de constr_pattern
herbelin
2000-04-30
*
Déplacement du type reference dans Term
herbelin
2000-04-28
*
Introduction d'un type constr_pattern pour les différents filtrages
herbelin
2000-04-26
*
Abstraction du type typed_type (un pas vers les jugements 2 niveaux)
herbelin
2000-04-20
*
Export gentermpr avec renommage
herbelin
2000-01-31
*
Abstraction de l'implémentation des signatures de Sign en vue intégration d...
herbelin
2000-01-26
*
Restructuration printer et parser
herbelin
2000-01-07
*
Nouveaux types 'constructor' et 'inductive' dans Term;
herbelin
1999-12-15
*
modules et coqc
filliatr
1999-12-12
*
Suppression Rel de rawconstr et correction de bugs d'affichage
herbelin
1999-12-10
*
Ajout des messages d'erreurs de Cases
herbelin
1999-12-09
*
Ajout des fonctions prpattern et prrawterm
herbelin
1999-12-01
*
printers
filliatr
1999-12-01
*
module Printer
filliatr
1999-11-26
[prev]