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
...
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Fix extract hyps to correctly discharge all hyps as described by keep
msozeau
2009-05-29
*
Fix implicit args code so that declarations are added for all
msozeau
2009-05-27
*
Uniformisation of some error messages + added test on setoid rewrite.
herbelin
2009-01-07
*
- Synchronized subst_object with load_object (load_and_subst_objects)
herbelin
2008-11-23
*
broke cyclic dependencies
barras
2008-07-24
*
Correct implementation of discharging of implicit arguments and add new
msozeau
2008-07-22
*
Documentation Prop<=Set et Arguments Scope Global
herbelin
2008-07-01
*
Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...
notin
2008-06-25
*
- Prise en compte des frozen state de Coq autant que possible pour
herbelin
2008-05-24
*
Correction bug #1842 + correction bug initialisation introduit dans
herbelin
2008-05-10
*
Add the ability to specify the implicit status of section variables and
msozeau
2008-04-02
*
Merge with lmamane's private branch:
lmamane
2008-02-22
*
Beaoucoup de changements dans la representation interne des modules.
soubiran
2008-02-01
*
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-12-06
*
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-12-05
*
Amélioration du message d'erreur dans end_module, end_module_type et close_s...
notin
2007-10-29
*
Merge with Lionel Elie Mamane's private branch:
lmamane
2007-01-10
*
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
*
Indentation + svnprop
notin
2006-09-12
*
Indentation + typo
notin
2006-09-01
*
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
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
Vérification qu'un module est ouvert avant d'insérer une déclaration nommÃ...
herbelin
2005-12-23
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Conformité au principe du nouveau warning X de ocaml 3.09
herbelin
2005-11-04
*
Keep ClosedSection marker for reset
herbelin
2005-02-20
*
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2005-02-18
*
Ajout du reset des numéros d'états dans reset_initial. Plus propre
coq
2005-02-10
*
Petit changement dans la gestion des nouveaux labels d'état (pour le
coq
2005-01-31
*
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
*
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
*
bug #780: compilation of several units in the same coqtop process
barras
2004-07-13
*
Crochets pour exported les sections en xml
herbelin
2004-03-27
*
Reset Initial uniquement interactivement
herbelin
2003-12-19
*
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
[prev]
[next]