index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
extraction
/
extract_env.ml
Age
Commit message (
Expand
)
Author
2001-11-12
suite du petit oups
letouzey
2001-11-12
petit oups
letouzey
2001-11-12
Refonte de extraction.ml. Traitement dans mlutil.ml des Empty Inductive (Texn)
letouzey
2001-11-08
Deplacement de l'optim singleton depuis extraction vers mlutil. Autres modifs...
letouzey
2001-11-05
optim: Idset au lieu de list
letouzey
2001-11-05
GROS COMMIT:
barras
2001-11-03
Creation de Recursive Extarction Module
letouzey
2001-10-30
legeres modifs pretty-print de l'extractions
letouzey
2001-10-26
Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ET...
letouzey
2001-10-23
suite du seisme
letouzey
2001-10-22
chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les o...
letouzey
2001-10-17
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-12
Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...
herbelin
2001-10-09
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-09-19
Changements de Extraction truc et Recursive Extraction
letouzey
2001-09-18
travail sur le Extract Constant
letouzey
2001-08-10
Parsing
herbelin
2001-05-14
mise en place extraction haskell
filliatr
2001-05-03
Changement de la structure des points fixes
barras
2001-04-24
Fin d'optimisation (cas modules) + warning pour coind & ocaml
letouzey
2001-04-24
cofix_warning dans les parametres d'extraction
filliatr
2001-04-23
Uncurryfy_ast inutile depuis l'eta-expansion dans extraction.ml.
letouzey
2001-04-20
optimizations extraction
filliatr
2001-04-19
cofix; axiomes; eta-expansions pour variables de types mal generalisees (en c...
filliatr
2001-04-10
réparation Correctness; options Extraction (changement de syntaxe)
filliatr
2001-04-09
branchement extraction en standard (pas de Require)
filliatr
2001-04-04
implification de extract_constr et extract_term
letouzey
2001-04-04
rollback sur les commandes Extract Constant/Inductive; nettoyage et documenta...
filliatr
2001-04-03
commandes Extract Constant/Inductive; message d'erreur pour les axiomes
filliatr
2001-04-02
ml_pop au lieu de ml_lift dans betared_ast
filliatr
2001-03-30
extraction modulaire
filliatr
2001-03-30
extraction modulaire + environnement des Fix corrigé
filliatr
2001-03-30
beta-reduction
filliatr
2001-03-28
changement type_var et signature
filliatr
2001-03-27
extraction recursive d'un morceau d'environnement
filliatr