index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
/
lib.mli
Commit message (
Expand
)
Author
Age
*
Merge from Lionel Elie Mamane's private branch:
lmamane
2007-01-10
*
Nouvelle approche pour le discharge modulaire
herbelin
2007-01-10
*
Cleaning backtracking code, optimized "Backtrack n x y" when n is
courtieu
2006-12-28
*
Modification de add_glob (support des modules dans Coqdoc)
notin
2006-05-23
*
Clarification role de library_part : renommage en remove_section_part
herbelin
2006-05-23
*
Keep ClosedSection marker for reset
herbelin
2005-02-20
*
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2005-02-18
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Ajout mémorisation numéro commande courante + reset vers ce numéro pour mo...
herbelin
2005-01-14
*
- Module/Declare Module syntax made more uniform:
sacerdot
2005-01-06
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
Nouvelle en-tête
herbelin
2004-07-16
*
Crochets pour exported les sections en xml
herbelin
2004-03-27
*
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
*
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
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Strengthenning rules for modules + No modules in sections
coq
2002-08-16
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
- condition de garde (suite)
barras
2001-12-10
*
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
*
Bug default module name (2eme)
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
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
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
*
Ajout d'une Nametab et d'un flag export aux ClosedSection; on applique export...
herbelin
2000-11-20
*
Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...
herbelin
2000-11-06
*
module_segment et module_filename
filliatr
2000-10-23
*
gros commit de tout ce que j'ai fait pendant les vacances :
filliatr
2000-01-21
*
modules
filliatr
1999-12-12
*
debug reset
filliatr
1999-12-10
*
- constantes avec recettes
filliatr
1999-12-09
*
deplacement de Discharge dans toplevel
filliatr
1999-12-08
*
add_leaf -> application methode cache
filliatr
1999-12-05
*
modifs pour premiere edition de liens
filliatr
1999-12-02
*
portage Astterm (partiellement)
filliatr
1999-11-29
*
with_heavy_rollback deplace dans States
filliatr
1999-09-29
[next]