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
...
*
Finalement, scopes utiles pour option 'where' (cf bug #1132)
herbelin
2006-04-07
*
Suppression du test Proof with <tac>
notin
2006-04-05
*
- correction du bug #1055
notin
2006-03-27
*
Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.
msozeau
2006-03-13
*
Correction du bug 808: il est maintenant interdit de déclarer une assomption...
coq
2006-03-02
*
Bug correction in saving proofs: If a hook opens a proof but does not close i...
bertot
2006-02-13
*
Messages nth branche
herbelin
2006-02-07
*
Amélioration des messages d'erreurs de tacred; unfold considère maintenant le
herbelin
2006-02-07
*
warning seulement si mode verbose
herbelin
2006-02-06
*
Message d'erreur si l'inductif d'une clause "in" d'un match n'a pas la
herbelin
2006-01-30
*
Réorganisation de la structure interne des types de déclarations (decl_kinds)
herbelin
2006-01-28
*
Suppression code pour hints nommés à la V7 (voire à la V6...)
herbelin
2006-01-28
*
Messages de idtac et fail peuvent maintenant être des listes de string, int ...
herbelin
2006-01-21
*
*** empty log message ***
coq
2006-01-16
*
Correction dans vernac_exact_proof -- jmn
coq
2006-01-16
*
Correction du bug #1055
coq
2006-01-13
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Prise en compte de notations numérales définies au niveau utilisateur+ lég...
herbelin
2006-01-08
*
Réorganisation; suppression code mort; documentation
herbelin
2006-01-07
*
Achèvement du commit incomplet de la révision 1.110 (cvs log toplevel/metas...
herbelin
2006-01-04
*
Mini-restructuration
herbelin
2005-12-30
*
Autres suppressions de composantes du traducteur
herbelin
2005-12-27
*
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...
herbelin
2005-12-26
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Changement de stratégie vis à vis du positionnement du module Top en mode b...
herbelin
2005-12-24
*
Simplifification de vernac_expr li l'abandon du traducteur
herbelin
2005-12-23
*
Correction printer des Tactic Notation
herbelin
2005-12-23
*
option '-top dir' now works also in batch mode (2ème)
herbelin
2005-12-22
*
option '-top dir' now works also in batch mode; it is even necessary to ensur...
herbelin
2005-12-22
*
Double bug de interp_modifiers anciennement caché par un troisième que les ...
herbelin
2005-12-22
*
Divers; restructuration des points d'entrée de Constrintern
herbelin
2005-12-21
*
Restructuration des points d'entrée de Pretyping et Constrintern
herbelin
2005-12-21
*
Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...
herbelin
2005-12-20
*
Suppression de la mise en boite automatique si format utilisateur
herbelin
2005-12-19
*
Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...
herbelin
2005-12-17
*
Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...
herbelin
2005-12-17
*
Orthographe de 'instantiate'
herbelin
2005-12-17
*
Changement des named_context
gregoire
2005-12-02
*
bug de coqide sous windows (bad file descriptor)
barras
2005-11-23
*
bug #909: Top n'est cree que si le contexte est vide
barras
2005-11-23
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
- debugging og "Show Intros": no line breaking + fresh ids
coq
2005-11-08
*
Point-virgule manquant ligne 914 détecté par nouveau warning X de ocaml 3.09
herbelin
2005-11-04
*
Types inductifs parametriques
mohring
2005-11-02
*
No parentheses around f in 'f \subst{...}'
herbelin
2005-05-26
*
Utilisation du module Buffer; encodage plus rigoureux des symboles en uri
herbelin
2005-05-26
*
Patch to avoid Whelp bug removed.
sacerdot
2005-05-26
*
New command: "Print Ltac qualid" to print user defined tactics.
sacerdot
2005-05-20
*
Interface vers outil de recherche Whelp
herbelin
2005-05-20
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
[prev]
[next]