index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
*
Amélioration message localisation constructions et modules
herbelin
2004-12-09
*
Bug (cf #892)
herbelin
2004-12-06
*
Amélioration message d'erreur v8
herbelin
2004-12-03
*
Complétion commit précédent
herbelin
2004-11-29
*
Réduire pour trouver l'arité d'une classe
herbelin
2004-11-26
*
Correction bug Notation: il faut re-déclarer les règles de parsing des nota...
herbelin
2004-11-22
*
compatibility with POWERPC
gregoire
2004-11-22
*
Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIRE
herbelin
2004-11-19
*
New command "Print Rewrite HindDb dbname".
sacerdot
2004-11-17
*
Ajout 'Locate Module'
herbelin
2004-11-17
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
*** empty log message ***
gregoire
2004-11-12
*
Changement dans les boxed values .
gregoire
2004-11-12
*
Prise en compte des notations récursives dans l'option 'format'
herbelin
2004-11-08
*
Non affichage des notations réduites à une variable
herbelin
2004-10-27
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Semble raisonnable de distinguer les noms aussi dans cant_apply
herbelin
2004-10-17
*
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
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
deplacement de clenv vers pretyping
barras
2004-09-03
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Bug List.hd vs list_last
herbelin
2004-09-03
*
MAJ options coqtop et coqc
herbelin
2004-09-03
*
Pas de notation v7 si purement en v8
herbelin
2004-08-23
*
Correction bug #830 : les noms des implicites temporaires étaient inconnus a...
herbelin
2004-08-23
*
Amélioration message d'erreur objet de récursion de type non inductif
herbelin
2004-08-06
*
"Print Setoids" command added.
sacerdot
2004-07-23
*
Backtrack sur l'utilisation de pa_macro car n'existait pas en 3.06
herbelin
2004-07-17
*
Abstraction vis à vis du type loc pour compatibilité ocaml 3.08
herbelin
2004-07-16
*
Branchement sur pa_macro, pa_ifdef devenant obsolete en 3.08
herbelin
2004-07-16
*
Nouvelle en-tête
herbelin
2004-07-16
*
bug #780: compilation of several units in the same coqtop process
barras
2004-07-13
*
bug #790: better error_not_clean
barras
2004-07-13
*
updated printing of evar context (may loop ?)
corbinea
2004-06-30
*
Correction bug #776
herbelin
2004-06-28
*
correspondance des records et noms de champs de records entre un module et sa...
letouzey
2004-06-25
*
Recherche de la source à partir de la gauche pour gérer des cas comme 'Coer...
herbelin
2004-06-02
*
Affichage de la date de checkout même si pas dans le répertoire de compilation
herbelin
2004-05-26
*
Correction bug 'Time Load foo'
herbelin
2004-05-25
*
test de conversion laissait echapper exception NotConvertible
barras
2004-05-14
*
pb facto des Fixpoint + erreur avec -dump-glob et Load
barras
2004-04-17
*
Export de l'information si un inductive est un record ou non (pour xml)
herbelin
2004-03-31
*
Distinction entre declarations internes (p.ex. _subproof) et declarations uti...
herbelin
2004-03-30
*
Distinction entre declarations internes (p.ex. _subproof) et declarations uti...
herbelin
2004-03-30
*
Nom qualifié pour option -top
herbelin
2004-03-28
*
Ajout option -top pour changer le nom 'Top' du toplevel
herbelin
2004-03-28
*
Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...
herbelin
2004-03-27
*
Ajout entree pour exporter les debuts et fins de compilation en mode -xml
herbelin
2004-03-26
[next]