index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
Commit message (
Expand
)
Author
Age
*
Refonte complete de la génération des types ML
letouzey
2002-03-26
*
An intuitionistic first-order theorem prover -- JProver.
huang
2002-03-22
*
reparation du test des reals
letouzey
2002-03-21
*
considerations de pretty-print
letouzey
2002-03-21
*
deux fichiers supplementaires de customisation d'extraction
letouzey
2002-03-21
*
changement du test extraction suite aux modif inining
letouzey
2002-03-21
*
modification de l'auto-inlining
letouzey
2002-03-21
*
renversement du renommage des variables
letouzey
2002-03-20
*
reparation du controle de l'apparition des termes
letouzey
2002-03-20
*
reorganisation des simplifications: letin eta-expansé apres le kill-dummy
letouzey
2002-03-20
*
un peu moins d'eta-expansion autour des Glob
letouzey
2002-03-20
*
bug optimize_fix fait trop tot
letouzey
2002-03-19
*
suite bug Dglob constant
letouzey
2002-03-19
*
bug avec les MLglob vraiment constants
letouzey
2002-03-19
*
travail sur les stratégies de réduction
letouzey
2002-03-19
*
remplacement des deux constants prop/arity par une seule dummy + pretty-print...
letouzey
2002-03-19
*
Fix d'un bug sur le test des inverses
delahaye
2002-03-19
*
Meilleure gestion de la reduction dans Field
delahaye
2002-03-17
*
epsilon
letouzey
2002-03-15
*
un peu de mise a jour de la doc extraction
letouzey
2002-03-15
*
evite les clash avec le type ocaml unit
letouzey
2002-03-15
*
gros commit: principalement ajout des lambdas arity + leur optimisation en te...
letouzey
2002-03-15
*
reparation semi setoid ring
clrenard
2002-03-14
*
Factorisation de la grammaire pour Extraction Language.
letouzey
2002-03-11
*
cas des constructeurs singletons. Messages d'erreur. Revision de test_extract...
letouzey
2002-03-05
*
Big commit extraction:
letouzey
2002-03-04
*
Nouveau Rewrite-in plus economique
barras
2002-03-04
*
Prise en compte des corps de letin dans les hypothèses
herbelin
2002-03-01
*
convert_hyp a change de type
barras
2002-03-01
*
Uniformisation convert_hyp
herbelin
2002-02-28
*
modifs des preambules d'extraction modulaire
letouzey
2002-02-27
*
pretty print des Cases devenant des let-in
letouzey
2002-02-25
*
code mort dans tactinterp; plus de Debug On/Off dans Correctness
filliatr
2002-02-21
*
Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parce
ddr
2002-02-20
*
petits changements cosmetiques sur les tactiques
barras
2002-02-15
*
suite et fin (?) de haskell: gestion des modules, mise en place du'un test
letouzey
2002-02-15
*
debut de gestion des open pour extraction modulaire
letouzey
2002-02-15
*
qq inline manuels (sigS_rec ...) + utilisation de library_part
letouzey
2002-02-14
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
suppression de la condition de la permutation case/fun
letouzey
2002-02-12
*
pretty print
letouzey
2002-02-12
*
Test & correction de la production de code Haskell
letouzey
2002-02-12
*
affichages avec prterm_env et non prterm; deb_print pour vraiment ne rien fai...
filliatr
2002-02-08
*
petit nettoyage de kernel/inductive
barras
2002-02-07
*
un assert false de trop (MLexn peut avoir des args)
letouzey
2002-02-07
*
oubli
letouzey
2002-02-06
*
gros changement dans mlutil.ml: ajout d'une elimination globale des prop
letouzey
2002-02-06
*
Ajout d'optimisations locales kill_prop
letouzey
2002-02-05
*
adaptation de l'extraction aux changements de Christine concernant rec/rect e...
letouzey
2002-01-31
*
extraction des CoInductives via les Lazy d'ocaml
letouzey
2002-01-31
[next]