index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
Makefile
Commit message (
Expand
)
Author
Age
...
*
tests automatiques
herbelin
2000-12-09
*
Suppresion de l'option -as, c'est maintenant -R qui devient l'option standard...
herbelin
2000-12-06
*
Portage d'AutoRewrite
delahaye
2000-12-02
*
Changement de la syntaxe des options -I et -R
herbelin
2000-11-30
*
Ajout d'une option d'alias à -I
herbelin
2000-11-29
*
Added -R inclusion to fix compilation in not-local configuration.
sacerdot
2000-11-28
*
-I inutiles pour coqc et utilisation de -R theories (pour garder trace des no...
herbelin
2000-11-28
*
Rajout de PolyListSyntax aussi dans Makefile
herbelin
2000-11-28
*
Xml contrib retached
sacerdot
2000-11-27
*
Ajout BEST partout a coqc
filliatr
2000-11-24
*
SearchPattern et SearchRewrite
filliatr
2000-11-24
*
Ajout d'une syntaxe pour Reals.
mayero
2000-11-23
*
retablissement de line_oriented_parser pour Yves
filliatr
2000-11-22
*
des proofs/macros qui trainaient dans le Makefile et le .depend
filliatr
2000-11-22
*
Ajout du clean pour tolink.ml
delahaye
2000-11-21
*
ln -sf au lieu de ln -s
filliatr
2000-11-21
*
implicites manuels
filliatr
2000-11-21
*
ajout de theories/Wellfounded
filliatr
2000-11-21
*
XML débranché
filliatr
2000-11-21
*
Prise en compte camlp4.opt dans la configuration et le Makefile
herbelin
2000-11-20
*
Prise en compte camlp4.opt dans la configuration et le Makefile
herbelin
2000-11-11
*
-I states dans les includes de Coq
filliatr
2000-11-09
*
-I theories/Init pour faire initial.coq
filliatr
2000-11-09
*
coqc appele avec -bindir bin
filliatr
2000-11-09
*
nouveau load path
filliatr
2000-11-08
*
tous les binaires maintenant dans le repertoire bin
filliatr
2000-11-08
*
Modification de la table des tactic Definitions pour eviter l'ecriture
mohring
2000-11-07
*
nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...
filliatr
2000-11-06
*
Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier deven...
herbelin
2000-11-05
*
Few OCaml files in contrib/xml
sacerdot
2000-11-03
*
compilation avec make de Solaris; README et INSTALL
filliatr
2000-11-03
*
compilation des fichiers ml4 sans GNUseries
filliatr
2000-11-03
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
- simplification Makefile (compilation des fichiers .ml'; pas encore parfait
filliatr
2000-10-31
*
Ajouts pour les tactiques utilisateur
delahaye
2000-10-30
*
g_natsyntax et g_zsyntax maintenant toujours linkes
filliatr
2000-10-27
*
ntrefiner.ml* removed in module xml
sacerdot
2000-10-26
*
xml contribution added to the Makefile
sacerdot
2000-10-25
*
MAJ
herbelin
2000-10-18
*
mise a jour dependances
filliatr
2000-09-18
*
Suppression Redinfo Sosub Abstraction
herbelin
2000-09-14
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Pattern -> parsing
delahaye
2000-07-21
*
portage Refine
filliatr
2000-07-20
*
Adaptation pour Alpha.
delahaye
2000-07-05
*
Adaptation pour alpha.
delahaye
2000-07-05
*
Utilisation du STRIP de config/Makefile pour gérer le mode profile
herbelin
2000-06-29
*
portage EAuto et Ring
filliatr
2000-06-21
*
dependance des CONTRIBVO envers initial.coq
filliatr
2000-06-12
*
Changement nom module Constant en Declarations
herbelin
2000-05-22
[prev]
[next]