index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
+ Adding an error message when the function cannot be defined
bertot
2006-02-03
*
maj
coq
2006-02-02
*
maj
coq
2006-02-01
*
protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)
barras
2006-02-01
*
protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)
barras
2006-02-01
*
New version of functional induction / inversion. By Julien Forest,
coq
2006-02-01
*
Optimisation filtrage sans lieurs (utile pour Ltac)
herbelin
2006-02-01
*
maj
coq
2006-01-31
*
Adaptation message d'erreur au cas des string
herbelin
2006-01-31
*
Ajout de fichiers d'interprétation de la syntaxe primitive pour string et char
herbelin
2006-01-31
*
Ajout décidabilité
herbelin
2006-01-31
*
maj
coq
2006-01-30
*
Suppression fonctions d'interprétation du vieux Case
herbelin
2006-01-30
*
Prise en compte coercions autour des sous-termes filtrés (si non dépendants)
herbelin
2006-01-30
*
Gestion des erreurs pour nombre incorrect d'argument des constructeurs (et de
herbelin
2006-01-30
*
- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer
herbelin
2006-01-30
*
Fonctions retournant les arits des constructeurs et inductifs (suite)
herbelin
2006-01-30
*
Déplacement du test du bon nombre d'argument des constructeurs (et de
herbelin
2006-01-30
*
Message d'erreur si l'inductif d'une clause "in" d'un match n'a pas la
herbelin
2006-01-30
*
Fonctions retournant les arits des constructeurs et inductifs
herbelin
2006-01-30
*
Nettoyage warning (dont flush et affichage seulement si mode verbose)
herbelin
2006-01-30
*
- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer;
herbelin
2006-01-30
*
Ajout ppenv
herbelin
2006-01-30
*
Plutôt pas de contraction des match dans le déboggueur
herbelin
2006-01-30
*
maj
coq
2006-01-29
*
Documentation
herbelin
2006-01-29
*
Ajout printer Idset.t
herbelin
2006-01-29
*
Bug 'match x in I' (potentiellement utilisable comme cast)
herbelin
2006-01-29
*
MAJ (synonymes de Lemma; auto using)
herbelin
2006-01-29
*
Ajout syntaxe concrète Proposition, synonyme de Lemma
herbelin
2006-01-29
*
maj
coq
2006-01-28
*
Réorganisation de la structure interne des types de déclarations (decl_kinds)
herbelin
2006-01-28
*
- Ajout syntaxe concrète Property/Corollary, synonymes de Lemma
herbelin
2006-01-28
*
- Ajout syntaxe concrète Property/Corollary, synonymes de Lemma
herbelin
2006-01-28
*
Correction bug Inspect introduit par le passage du discharge à une méthode ...
herbelin
2006-01-28
*
Ajout option 'using lemmas' à auto/trivial/eauto
herbelin
2006-01-28
*
Suppression code pour hints nommés à la V7 (voire à la V6...)
herbelin
2006-01-28
*
maj
coq
2006-01-27
*
maj
coq
2006-01-26
*
maj
coq
2006-01-25
*
exporting the global reference to the inductive " \/ " in coqlib and
bertot
2006-01-25
*
maj
coq
2006-01-24
*
Suppression de la dépendance en Map.fold de ocaml dont la sémantique a
herbelin
2006-01-24
*
maj
coq
2006-01-23
*
Oubli lors suppression traducteur
herbelin
2006-01-23
*
Répercussion mise à jour de Pierre Casteran vis à vis du changement de sta...
herbelin
2006-01-23
*
Precision
herbelin
2006-01-23
*
maj
coq
2006-01-22
*
Application de la suggestion de Nicolas Magaud (#1060)
herbelin
2006-01-22
*
maj
coq
2006-01-21
[next]