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
*
make reals prend en compte tous les .vo de theories/Reals
filliatr
2001-04-25
*
Suppression d'une partie de code commente
delahaye
2001-04-24
*
README avec ref (2)
letouzey
2001-04-24
*
TODO in v.o., test/Makefile moins pire, README avec ref
letouzey
2001-04-24
*
Ajout du .depend
mohring
2001-04-24
*
Retire theories/Num
mohring
2001-04-24
*
Correction typos
mohring
2001-04-24
*
ajout d'un fichier README
letouzey
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-24
*
Removing a debug message for the search command.
bertot
2001-04-24
*
forme code
filliatr
2001-04-23
*
mise a jour
letouzey
2001-04-23
*
realisation des reals
letouzey
2001-04-23
*
Gros nain avec de Bruijn...
letouzey
2001-04-23
*
divers
filliatr
2001-04-23
*
nettoyage
filliatr
2001-04-23
*
expansion des constr purs
filliatr
2001-04-23
*
Uncurryfy_ast inutile depuis l'eta-expansion dans extraction.ml.
letouzey
2001-04-23
*
Remaniement Makefile de test. make reals possible
letouzey
2001-04-23
*
Ajout Fourier
mayero
2001-04-20
*
optimizations extraction
filliatr
2001-04-20
*
Ajout des entetes
delahaye
2001-04-20
*
nettoyage
filliatr
2001-04-20
*
Add a treatement of elaborate Intros tactics, CONJPATTERN and family.
bertot
2001-04-19
*
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
*
ZArith --> Zarith
mohring
2001-04-19
*
synchonization des tables d'extraction
filliatr
2001-04-19
*
remplace Zarith par ZArith
mohring
2001-04-19
*
modifs des scripts de test auto
filliatr
2001-04-19
*
deplacement de l'optimisation inductif singleton
letouzey
2001-04-19
*
script de bench automatique pour extraction
letouzey
2001-04-19
*
Making sure there will be no warnings at compile time.
bertot
2001-04-19
*
Ajout de Field
delahaye
2001-04-19
*
Correcting a problem of s that appears behind a Let when there are
bertot
2001-04-18
*
Changing the commands to switch to textual explanation of proofs.
bertot
2001-04-18
*
Adding files for the production of textual explanations as used in pcoq.
bertot
2001-04-18
*
eliminiation des singletons du genre sig + divers
letouzey
2001-04-13
*
nouvelle gestion des variables de type ML
letouzey
2001-04-12
*
documentation automatique de la bibliothèque standard
filliatr
2001-04-11
*
réparation d'un bug de Correctness: whd_programs ne doit pas réduire les te...
filliatr
2001-04-11
*
bug dans eta-expansion des constructeurs. Argument Prop dans extract_type_app
letouzey
2001-04-10
*
portage exemples Correctness; changement du nom de pred_of_minus dans coq_omega
filliatr
2001-04-10
*
réparation Correctness; options Extraction (changement de syntaxe)
filliatr
2001-04-10
*
bug lift dans IsRel de extract_type. Axiomes dans extract_type
letouzey
2001-04-10
*
exemples Correctness
filliatr
2001-04-09
*
branchement extraction en standard (pas de Require)
filliatr
2001-04-09
*
réparation Quote
filliatr
2001-04-09
[next]