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
...
*
Logic_TypeSyntax disparu
herbelin
2003-10-11
*
Death of 'a somewhat cryptic module'
herbelin
2003-10-11
*
Death of 'a somewhat cryptic module'
herbelin
2003-10-11
*
mise a jour nouvelle syntaxe
barras
2003-10-11
*
maj
filliatr
2003-10-10
*
Suppression Grammar/Syntax
herbelin
2003-10-10
*
identity est equivalent sur Type (sauf sans argument)
herbelin
2003-10-10
*
nat_scope ouvert par defaut
herbelin
2003-10-10
*
identity est equivalent sur Type (sauf sans argument)
herbelin
2003-10-10
*
type_scope
herbelin
2003-10-10
*
Suppression de definitions equivalentes
herbelin
2003-10-10
*
Bug undo
herbelin
2003-10-10
*
Notation '^'
herbelin
2003-10-10
*
*** empty log message ***
herbelin
2003-10-10
*
Plus d'Eval Compute
herbelin
2003-10-10
*
MAJ commentaires
herbelin
2003-10-10
*
MAJ
herbelin
2003-10-10
*
Typo
herbelin
2003-10-10
*
Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'
herbelin
2003-10-10
*
Delimiters N devient 'nat'
herbelin
2003-10-10
*
Cablage en dur de inversion
herbelin
2003-10-10
*
code mort
herbelin
2003-10-10
*
show_subgoals dans Pfedit
herbelin
2003-10-10
*
Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'
herbelin
2003-10-10
*
MAJ .v8
herbelin
2003-10-10
*
pf_get_new_id en provenance de feu wcclausenv
herbelin
2003-10-10
*
Suppression clenv_change_head que seul Wcclausenv utisait
herbelin
2003-10-10
*
Dead of 'a somewhat cryptic module'
herbelin
2003-10-10
*
Dead of 'a somewhat cryptic module' (Inv doesn't use applyUsing any longer; p...
herbelin
2003-10-10
*
Ajout printers pour constr et constr_pattern (sans traduction)
herbelin
2003-10-10
*
Unification lemInv et lemInv_in
herbelin
2003-10-10
*
pr_tactic sans traduction; affichage Inversion
herbelin
2003-10-10
*
Cablage en dur de inversion
herbelin
2003-10-10
*
Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'
herbelin
2003-10-10
*
Intégration de la premiere partie de 'hightactics' dans 'tactics' suite à c...
herbelin
2003-10-10
*
Affichage des buts par Pfedit pour utilisation par les tactiques
herbelin
2003-10-10
*
Affichage des buts par Pfedit pour utilisation par les tactiques (Setoid_repl...
herbelin
2003-10-10
*
Gestion en temps constant de la pile des Unfo; affichage des buts par Pfedit ...
herbelin
2003-10-10
*
Gestion en temps constant de la pile des Unfo
herbelin
2003-10-10
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
Cacher les .v8
herbelin
2003-10-10
*
Renommage en v8 de PolyList en List et List en MonoList
herbelin
2003-10-10
*
Renommage en v8 de PolyList en List et List en MonoList
herbelin
2003-10-10
*
Nouveau format de l'option 'format'
herbelin
2003-10-09
*
Compatibilite ocaml 3.06 et 3.07
herbelin
2003-10-09
*
Syntaxe VernacEndProof changee pour ajout mot-cle 'Admitted'
herbelin
2003-10-09
*
Teste interaction ltac et modules
herbelin
2003-10-08
*
Ajout exemple parametres implicites
herbelin
2003-10-08
*
Bug utilisation nametab pour ltac
herbelin
2003-10-08
*
Pb residuel avec la prise en compte des parametres implicites d'inductifs
herbelin
2003-10-08
[prev]
[next]