index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
pretty.mli
Commit message (
Expand
)
Author
Age
*
Export a function (build_inductive) that is used in the graphical interface.
bertot
2001-04-03
*
amelioration de la structure des univers
barras
2001-03-28
*
entetes
filliatr
2001-03-15
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Prise en compte noms longs dans divers fonctions de Print
herbelin
2000-11-26
*
SearchPattern et SearchRewrite
filliatr
2000-11-24
*
Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp;
herbelin
2000-11-23
*
deplacement poly_args; iterateurs sur les segments
filliatr
2000-11-22
*
Prise en compte des noms qualifiés dans certaines commandes
herbelin
2000-11-20
*
Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...
herbelin
2000-11-06
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
Suite restructuration inductifs; changement nom module Constant en Declarations
herbelin
2000-05-22
*
Effets de bords suite à la restructuration des inductives (cf Inductive)
herbelin
2000-05-18
*
Intégration du Termast et du Retyping de HH, et modifications connexes
herbelin
1999-12-01
*
- environment -> safe_environment
filliatr
1999-12-01
*
portage Astterm (partiellement)
filliatr
1999-11-29
*
module Pretty (partiellement)
filliatr
1999-11-26