index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
Commit message (
Expand
)
Author
Age
*
Changement des named_context
gregoire
2005-12-02
*
Fonctionnalisation du cache 'compunit' pour réparer correctement le bug #103...
herbelin
2005-11-26
*
bug #909: Top n'est cree que si le contexte est vide
barras
2005-11-23
*
Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)
herbelin
2005-11-21
*
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
*
Types inductifs parametriques
mohring
2005-11-02
*
Correction bug #1030 (conséquence du commit 1.84 sur le discharge: add_froze...
herbelin
2005-11-01
*
Adoption du nom canonique global_of_constr pour éviter confusion avec type r...
herbelin
2005-05-20
*
Keep ClosedSection marker for reset
herbelin
2005-02-20
*
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2005-02-18
*
Standardisation of constr_of_reference into constr_of_global + Moved Indmap a...
herbelin
2005-02-18
*
Code mort
herbelin
2005-02-18
*
Ajout du reset des numéros d'états dans reset_initial. Plus propre
coq
2005-02-10
*
Nettoyage et documentation de Library
herbelin
2005-02-06
*
Localisation des libraries compilées uniquement via la structure du loadpath...
herbelin
2005-02-05
*
Petit changement dans la gestion des nouveaux labels d'état (pour le
coq
2005-01-31
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed
sacerdot
2005-01-14
*
Ajout mémorisation numéro commande courante + reset vers ce numéro pour mo...
herbelin
2005-01-14
*
Construct "T with (Definition|Module) id := c" generalized to
sacerdot
2005-01-13
*
- Module/Declare Module syntax made more uniform:
sacerdot
2005-01-06
*
HUGE COMMIT
sacerdot
2005-01-03
*
Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...
herbelin
2005-01-02
*
Bug 'Locate Library lib' quand 'lib' est aussi un module
herbelin
2004-11-17
*
dead (and obsolete) code (in comments) removed
sacerdot
2004-11-16
*
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
*
code mort
herbelin
2004-11-09
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Prise en compte dans cut_ident des idents de la form _23 qui sont officiellem...
herbelin
2004-10-12
*
option -no-hash-consing pour supprimmer le hash-consing
filliatr
2004-10-12
*
Suppression IsConjecture redondant avec Conjectural
herbelin
2004-10-11
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
Nouvelle en-tête
herbelin
2004-07-16
*
bug #780: compilation of several units in the same coqtop process
barras
2004-07-13
*
correspondance des records et noms de champs de records entre un module et sa...
letouzey
2004-06-25
*
MAJ numéro magique
herbelin
2004-04-14
*
Export de l'information si un inductive est un record ou non (pour xml)
herbelin
2004-03-31
*
The XML exportation hook for require is now active for:
sacerdot
2004-03-30
*
Distinction entre declarations internes (p.ex. _subproof) et declarations uti...
herbelin
2004-03-30
*
Crocret xml pour Require
herbelin
2004-03-29
*
Crochets pour exported les sections en xml
herbelin
2004-03-27
*
Memorisation du type de variable (Hyp or Var)
herbelin
2004-03-26
*
preparation packages V8.0-cdrom
barras
2004-03-15
*
Bug de Require multiple
herbelin
2004-01-28
*
meilleure presentation des commentaires du traducteur
barras
2004-01-02
*
Changement numero magique; message d'erreur en cas de mauvaise syntaxe
herbelin
2003-12-23
*
Reset Initial uniquement interactivement
herbelin
2003-12-19
*
name_app accessible a tous dans Nameops
herbelin
2003-12-19
[next]