index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
/
lib.ml
Commit message (
Expand
)
Author
Age
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...
herbelin
2003-09-12
*
CoqIde : but reset_mod
filliatr
2003-05-19
*
configure et make install s'occupent de CoqIde tout seuls
filliatr
2003-05-19
*
ajout d'une fonction reset_mod
monate
2003-03-26
*
Pour satisfaire ProofGeneral
coq
2003-01-31
*
Petit netoyage dans lib
coq
2002-12-19
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Strengthenning rules for modules + No modules in sections
coq
2002-08-16
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
compat ocaml 3.03
filliatr
2001-12-13
*
- condition de garde (suite)
barras
2001-12-10
*
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-12
*
corrections mineures suite au commit de restructuration du noyau
barras
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-17
*
Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et le...
herbelin
2001-09-19
*
Mise en place de noms contenant la section pour Fact et Remark
herbelin
2001-09-18
*
Rétablissement de Print Section
herbelin
2001-09-06
*
Bug default module name (2eme)
herbelin
2001-09-06
*
Bug default module name
herbelin
2001-09-06
*
Parsing
herbelin
2001-08-10
*
Avertissement contre les Require dans le corps d'une section
herbelin
2001-07-05
*
entetes
filliatr
2001-03-15
*
bug Reset et Sections
filliatr
2001-02-28
*
Test pour empêcher 2 sections de même noms
herbelin
2000-12-20
*
Pédagogie
herbelin
2000-12-19
*
Bug des locaux au premier niveau des modules qui disparaissaient de l'environ...
herbelin
2000-12-15
*
Reparation conditions de positivites inductifs, echange dans add_entry
mohring
2000-12-06
*
La zone par défaut pour le nommage des modules est Scratch
herbelin
2000-11-29
*
Prise en compte du repertoire dans le section path; utilisation de dirpath po...
herbelin
2000-11-28
*
Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab
filliatr
2000-11-24
*
certains effets disparaissent a la sortie des sections, d'autres non (selon S...
filliatr
2000-11-24
*
reset_name: try / with juste autour de find_entry_p (=> propage les
filliatr
2000-11-21
*
ajout d'un frozen_state après la fermeture d'une section (sinon bug !)
filliatr
2000-11-21
*
correction bug Reset
filliatr
2000-11-21
*
separation calcul des implicites et declaration des constantes / inductifs / ...
filliatr
2000-11-21
*
Petit bug entre close_section's
herbelin
2000-11-20
*
Ajout d'une Nametab et d'un flag export aux ClosedSection; on applique export...
herbelin
2000-11-20
*
methode export
filliatr
2000-11-15
*
Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...
herbelin
2000-11-06
*
Bug pop_path_prefix : List.rev manquant
herbelin
2000-10-25
*
correction bug univers (dummy_univ)
filliatr
2000-10-06
*
bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...
filliatr
2000-06-21
*
gros commit de tout ce que j'ai fait pendant les vacances :
filliatr
2000-01-21
*
sauvegarde de la valeur de module_name
filliatr
1999-12-14
*
mise a jour de refiner.ml (reports de modifs de la V6.3)
barras
1999-12-13
*
modules
filliatr
1999-12-12
*
debug reset
filliatr
1999-12-10
*
- constantes avec recettes
filliatr
1999-12-09
[next]