index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
extraction
/
extraction.ml
Commit message (
Expand
)
Author
Age
*
cas des constructeurs singletons. Messages d'erreur. Revision de test_extract...
letouzey
2002-03-05
*
Big commit extraction:
letouzey
2002-03-04
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
Test & correction de la production de code Haskell
letouzey
2002-02-12
*
gros changement dans mlutil.ml: ajout d'une elimination globale des prop
letouzey
2002-02-06
*
adaptation de l'extraction aux changements de Christine concernant rec/rect e...
letouzey
2002-01-31
*
maj CHANGES extraction + bug extraction & _
letouzey
2001-12-21
*
Pour ocamlweb ...
letouzey
2001-12-18
*
anti revolution culturelle: retour des arguments logiques
letouzey
2001-12-18
*
compat ocaml 3.03
filliatr
2001-12-13
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
Revolution culturelle: suppression des arguments prop
letouzey
2001-11-14
*
suite refonte extraction.ml
letouzey
2001-11-12
*
Refonte de extraction.ml. Traitement dans mlutil.ml des Empty Inductive (Texn)
letouzey
2001-11-12
*
Deplacement de l'optim singleton depuis extraction vers mlutil. Autres modifs...
letouzey
2001-11-08
*
Refonte du fichier mlutil.ml. Correction d'un bug d'optim case
letouzey
2001-11-07
*
GROS COMMIT:
barras
2001-11-05
*
message non barbare si extraction dans une section
letouzey
2001-11-05
*
suite des modifs concernant les optimisations divers
letouzey
2001-11-02
*
chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les o...
letouzey
2001-10-22
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
correction du eta_expanse
letouzey
2001-09-20
*
utilisation du nouveau get_sort_family_of
letouzey
2001-09-20
*
Verification supplementaire avant optimisation singleton
letouzey
2001-09-19
*
Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...
herbelin
2001-07-21
*
Nettoyage/restructuration des ensembles d'indicateurs de réductions
herbelin
2001-07-02
*
2 bugs: typevarlist pour inductifs + args pour flexibles
letouzey
2001-06-22
*
ordre des inductifs + axiome-type
letouzey
2001-05-22
*
bug cast
letouzey
2001-05-11
*
retouche de extract_inductive_declaration
letouzey
2001-05-10
*
nettoyage extraction
filliatr
2001-05-09
*
cleanup + comments, toujours
letouzey
2001-05-09
*
commentaires
letouzey
2001-05-04
*
Changement de la structure des points fixes
barras
2001-05-03
*
commentaires sur renommages des var dans extract_type
letouzey
2001-05-02
*
cleanup, comments
letouzey
2001-04-30
*
ocamlweb
filliatr
2001-04-30
*
commentaires mlutil + binders_fold en cours
letouzey
2001-04-30
*
Fin d'optimisation (cas modules) + warning pour coind & ocaml
letouzey
2001-04-24
*
Uncurryfy_ast inutile depuis l'eta-expansion dans extraction.ml.
letouzey
2001-04-23
*
optimizations extraction
filliatr
2001-04-20
*
scripts; extraction False_rec
filliatr
2001-04-19
*
blindage False_rec
filliatr
2001-04-19
*
cofix; axiomes; eta-expansions pour variables de types mal generalisees (en c...
filliatr
2001-04-19
*
synchonization des tables d'extraction
filliatr
2001-04-19
*
deplacement de l'optimisation inductif singleton
letouzey
2001-04-19
*
nouvelle gestion des variables de type ML
letouzey
2001-04-12
*
bug dans eta-expansion des constructeurs. Argument Prop dans extract_type_app
letouzey
2001-04-10
*
bug lift dans IsRel de extract_type. Axiomes dans extract_type
letouzey
2001-04-10
*
axiomes dans les types
filliatr
2001-04-04
[next]