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
...
*
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
*
patch Omega (bug 129)
filliatr
2002-01-25
*
In Pcoq, the search commands had an erroneous behavior. Bound variables
bertot
2002-01-23
*
Correction de Pierre Crégut pour le bug MERGE_EQ
herbelin
2002-01-21
*
Zinv -> Zopp
filliatr
2002-01-21
*
Bug MERGE_EQ
herbelin
2002-01-18
*
Plusieurs arguments autorisés pour Require et Read Module
herbelin
2002-01-18
*
ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de contr...
letouzey
2002-01-18
*
Orthographe
herbelin
2002-01-11
*
maj CHANGES extraction + bug extraction & _
letouzey
2001-12-21
*
contrib/interface/dad.ml4 had no real need of streams, it should have been
bertot
2001-12-19
*
debranchement du test sur les Reals
letouzey
2001-12-19
*
reparation du make depend et du .depend
letouzey
2001-12-19
*
Corrections post contournement des streams avec ++
herbelin
2001-12-19
*
the function Ctast.section_path was wrong. It performed two reverse
bertot
2001-12-18
*
Pour ocamlweb ...
letouzey
2001-12-18
*
Oubli d'un quote
herbelin
2001-12-18
*
There remained traces of streams with the old syntax.
bertot
2001-12-18
*
Integrating the Ltac language and the Blast tool into the interface
bertot
2001-12-18
*
typo de parenthèsage + suppression de string (= str maintenant)
letouzey
2001-12-18
*
anti revolution culturelle: retour des arguments logiques
letouzey
2001-12-18
*
ote les redondances des entetes
letouzey
2001-12-18
*
le save de Correctness faisant assert false
barras
2001-12-17
*
compat ocaml 3.03
filliatr
2001-12-13
*
correction de bugs concernant la gestion des modules. debranchement du test d...
letouzey
2001-12-10
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
remise au gout du jour du repertoire theories/Sorting de la V6.3
letouzey
2001-11-21
*
Make sure that NatRing won't loop forever.
bertot
2001-11-21
*
hack temporaire concernant les remarks/modules
letouzey
2001-11-20
[prev]
[next]