index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2001-05-11
m.a.j. PROBLEMES/TODO
letouzey
2001-05-11
construct_reference regarde d'abord dans le contexte local, puis les globaux
filliatr
2001-05-10
exemples Magic
letouzey
2001-05-10
message 'is defined' seulement en mode verbose
filliatr
2001-05-10
retouche de extract_inductive_declaration
letouzey
2001-05-10
ajout d'un afficher de contexte et d'une fonction constbody_of_string
letouzey
2001-05-10
Bug lift de la contrainte au passage du let (bug rapporte par S. Boulme)
herbelin
2001-05-09
nettoyage extraction
filliatr
2001-05-09
cleanup + comments, toujours
letouzey
2001-05-07
ex d'utilisation de fourier avec field
mayero
2001-05-07
integration de field a fourier
mayero
2001-05-07
quelques bug reports mineurs
barras
2001-05-04
commentaires
letouzey
2001-05-03
Changement de la structure des points fixes
barras
2001-05-02
commentaires sur renommages des var dans extract_type
letouzey
2001-04-30
cleanup, comments
letouzey
2001-04-30
ocamlweb
filliatr
2001-04-30
commentaires mlutil + binders_fold en cours
letouzey
2001-04-25
ajout pour le cdrom
mayero
2001-04-25
Notes pour la version Windows
delahaye
2001-04-25
*** empty log message ***
courant
2001-04-25
*** empty log message ***
courant
2001-04-25
*** empty log message ***
courant
2001-04-25
ligne vide lors de l'affichage des messages d'erreur a toplevel entre
barras
2001-04-25
message d'erreur pour rattrapper l'anomalie avec SQUASH
barras
2001-04-25
make -j world -> make world en raison de bug ocamlc/ocamlopt
courant
2001-04-25
man pages for coq-interface and parser
courant
2001-04-25
Ajout pages de man coq_makefile et coqmktop
courant
2001-04-25
modif pour RPM et Debian
courant
2001-04-25
modif rpm
courant
2001-04-25
make reals prend en compte tous les .vo de theories/Reals
filliatr
2001-04-25
coqweb
filliatr
2001-04-25
- Ajout pages de man pour coqc, coqtop, coqtop.opt et coqtop.byte
courant
2001-04-25
Amelioration message args constructeur
herbelin
2001-04-25
Bug perte d'alias avec type dependents
herbelin
2001-04-25
Amelioration affichage
herbelin
2001-04-25
MAJ
herbelin
2001-04-25
MAJ
herbelin
2001-04-24
SearchIsos n'a pas encore ete porte
delahaye
2001-04-24
Messages d'erreur Cases
herbelin
2001-04-24
correction nom
mayero
2001-04-24
Les clauses de Rec doivent prendre des tactic_atom's
delahaye
2001-04-24
Suppression d'une partie de code commente
delahaye
2001-04-24
Ajout du cas True->A|-B
delahaye
2001-04-24
interdiction occ positives ET negatives dans Pattern
werner
2001-04-24
Reorganisation pour Ltac
delahaye
2001-04-24
Mise a jour V7
mohring
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
[next]