index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
extraction
Commit message (
Expand
)
Author
Age
*
Reecriture du extract_type pour Prod et Lambda. Eta-expansion dans les branch...
letouzey
2001-03-21
*
affichage declarations fix + bug extraction sumbool_rec mis a jour
filliatr
2001-03-20
*
mlutil
filliatr
2001-03-20
*
extraction naive de fix et case
filliatr
2001-03-20
*
Extract_term_with_type. mise a jour & verification des commentaires
letouzey
2001-03-20
*
entetes
filliatr
2001-03-15
*
interface du extract_rec. Extract_constr prend un environnement
letouzey
2001-03-14
*
signatures dans le bon ordre
filliatr
2001-03-13
*
Finite
filliatr
2001-03-13
*
simplification: plus de contexte pour extract_type et contexte simplifié pou...
filliatr
2001-03-13
*
suite de la verification des assert false
letouzey
2001-03-13
*
fin du letin
letouzey
2001-03-12
*
debut let in
filliatr
2001-03-12
*
mise a jour commentaires'
filliatr
2001-03-12
*
Commentaires. Verification des assert false. Probleme des types ML arity.
letouzey
2001-03-12
*
distinction contexte et signature
filliatr
2001-03-07
*
plus de commentaires
letouzey
2001-03-06
*
ocamlweb
filliatr
2001-03-05
*
extraction termes (suite)
filliatr
2001-03-05
*
indentation code
filliatr
2001-03-05
*
debut extraction termes; pp lambda
filliatr
2001-02-27
*
ajout Vprop, Tprop et Eprop
filliatr
2001-02-26
*
extraction des types et des inductifs
filliatr
2001-02-22
*
nouveau design ou le renommage sera fait a posteriori
filliatr
2001-02-21
*
mise en place fichiers extraction
filliatr
2001-02-20
*
mise en place extraction
filliatr
2001-02-06