index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
extraction
/
ocaml.ml
Commit message (
Expand
)
Author
Age
*
mise en place extraction haskell
filliatr
2001-05-14
*
Changement de la structure des points fixes
barras
2001-05-03
*
Fin d'optimisation (cas modules) + warning pour coind & ocaml
letouzey
2001-04-24
*
cofix_warning dans les parametres d'extraction
filliatr
2001-04-24
*
Uncurryfy_ast inutile depuis l'eta-expansion dans extraction.ml.
letouzey
2001-04-23
*
optimizations extraction
filliatr
2001-04-20
*
synchonization des tables d'extraction
filliatr
2001-04-19
*
deplacement de l'optimisation inductif singleton
letouzey
2001-04-19
*
eliminiation des singletons du genre sig + divers
letouzey
2001-04-13
*
branchement extraction en standard (pas de Require)
filliatr
2001-04-09
*
axiomes dans les types
filliatr
2001-04-04
*
commandes Extract Constant/Inductive; message d'erreur pour les axiomes
filliatr
2001-04-03
*
parenthèses autour des types dans les arguments des constructeurs
filliatr
2001-04-02
*
underscores pour les variables représentant des propositions
filliatr
2001-04-02
*
inductifs vides
filliatr
2001-04-02
*
ml_pop au lieu de ml_lift dans betared_ast
filliatr
2001-04-02
*
extraction modulaire
filliatr
2001-03-30
*
extraction modulaire + environnement des Fix corrigé
filliatr
2001-03-30
*
changement type_var et signature
filliatr
2001-03-28
*
extraction recursive d'un morceau d'environnement
filliatr
2001-03-27
*
eta-expansion des constructeurs si necessaire (a posteriori en miniML)
filliatr
2001-03-23
*
affichage declarations fix + bug extraction sumbool_rec mis a jour
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
*
Commentaires. Verification des assert false. Probleme des types ML arity.
letouzey
2001-03-12
*
distinction contexte et signature
filliatr
2001-03-07
*
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