index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
detyping.mli
Commit message (
Expand
)
Author
Age
*
Add functionality to permit printing terms with references to anonymous varia...
msozeau
2007-02-16
*
Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort
herbelin
2006-05-19
*
- Distinction explicite des parties paramètres et arguments dans le type
herbelin
2006-04-27
*
- Utilisation d'abbréviations pour les types intervenant dans RCases
herbelin
2006-04-26
*
Version préliminaire d'inversion de la compilation du filtrage
herbelin
2006-01-16
*
Standardisation du nom de subst_raw en subst_rawconstr
herbelin
2006-01-11
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Documentation
herbelin
2005-05-20
*
HUGE COMMIT
sacerdot
2005-01-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
Suppression de Rawterm.loc, branchement sur Util.loc
herbelin
2004-07-16
*
Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...
herbelin
2004-03-28
*
Changement de l'afficheur pour que les variables liées aient un nom indépen...
herbelin
2003-09-23
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Factorisation de detype_case pour utilisation par l'afficheur de pattern
herbelin
2003-06-10
*
petit nettoyage de kernel/inductive
barras
2002-02-07
*
GROS COMMIT:
barras
2001-11-05
*
entetes
filliatr
2001-03-15
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Renommage canonique :
herbelin
2000-10-18
*
Suppression de Abst
herbelin
2000-09-10
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
Prise en compte nouveau case_info
herbelin
2000-03-21
*
Traduction constr->rawconstr (avant dans Termast
herbelin
2000-01-07