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
*
-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
*
Restructuration des outils pour les inductifs.
herbelin
2000-05-18
*
Intégration de leminv
herbelin
2000-05-05
*
Vernacinterp passe après Command
herbelin
2000-05-04
*
nettoyage (quelques oublis dans make clean)
filliatr
2000-05-03
*
compilation bytecode / native :
filliatr
2000-05-03
*
Ajout du langage de tactiques
delahaye
2000-05-03
*
portage Omega (mais toujours pas Zpower et Zlogarithm)
filliatr
2000-05-02
*
MAJ
herbelin
2000-04-30
*
MAJ
herbelin
2000-04-28
*
portage Omega (code seulement)
filliatr
2000-04-28
*
portage en ocaml / camlp4 3.00
filliatr
2000-04-28
*
Débranchement provisoire equality et tauto
herbelin
2000-04-26
*
Compilation pbs (coqc not finding coqtop, coqc not finding .vo when
courant
2000-04-21
*
- bug make_module_marker (plus de # et de .obj maintenant)
filliatr
2000-03-21
*
Tauto
filliatr
2000-03-20
*
ZArith
filliatr
2000-03-18
*
on ne compile pas Div.v (Realizer)
filliatr
2000-03-18
*
theories/Bool
filliatr
2000-03-16
*
Eqdep_dec doit etre compile
filliatr
2000-03-10
*
compilation theories/Arith
filliatr
2000-03-10
*
Ajout theories/Logic/*.vo
herbelin
2000-03-08
[next]