index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
/
constrextern.mli
Commit message (
Expand
)
Author
Age
...
*
Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...
herbelin
2005-01-02
*
Mecanisme d'affichage des types (notamment les conclusions des buts) typiquem...
herbelin
2004-12-22
*
Abstraction vis à vis du type loc pour compatibilité ocaml 3.08
herbelin
2004-07-16
*
Nouvelle en-tête
herbelin
2004-07-16
*
Debranchement de l'affichage systematique des projections avec la notation po...
herbelin
2003-10-16
*
Scope type pour le codomaine de Prod aussi; ajout extern_rawtype
herbelin
2003-09-12
*
Traducteur de correctness
herbelin
2003-08-14
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Amélioration afficheur de Cases pour les constr_pattern
herbelin
2003-06-10
*
Mécanisme plus simple et efficace pour traduire les implicites
herbelin
2003-04-09
*
*** empty log message ***
barras
2003-03-12
*
Problèmes et améliorations divers affichage
herbelin
2002-12-09
*
Re-déplacement du résultat de Grammar au niveau constr_expr
herbelin
2002-12-02
*
Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...
herbelin
2002-11-24
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
[prev]