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
*
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
*
implification de extract_constr et extract_term
letouzey
2001-04-04
*
supression vieux fichiers extraction
filliatr
2001-04-04
*
rollback sur les commandes Extract Constant/Inductive; nettoyage et documenta...
filliatr
2001-04-04
*
commandes Extract Constant/Inductive; message d'erreur pour les axiomes
filliatr
2001-04-03
*
underscores pour les variables représentant des propositions
filliatr
2001-04-02
*
extraction modulaire + environnement des Fix corrigé
filliatr
2001-03-30
*
application avec bcp args
letouzey
2001-03-30
*
changement type_var et signature
filliatr
2001-03-28
*
conservation des arguments dans Prop (snif)
filliatr
2001-03-27
*
extraction recursive d'un morceau d'environnement
filliatr
2001-03-27
*
trace des inductifs sur Prop
letouzey
2001-03-27
*
cache pour les constantes
filliatr
2001-03-26
*
eta-expansion des constructeurs si necessaire (a posteriori en miniML)
filliatr
2001-03-23
*
suppression des param dans inductifs. suite du Cases
letouzey
2001-03-23
*
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
*
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
*
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
[next]