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
*
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
*
Prise en compte des paramètres implicites d'inductifs pour la globalisation ...
herbelin
2003-10-08
*
Des abbreviations pour constrintern.ml; generic argument IdentArg
herbelin
2003-10-08
*
Des abbreviations pour constrintern.ml
herbelin
2003-10-08
*
Test Conjecture
herbelin
2003-10-08
*
MAJ
herbelin
2003-10-08
*
Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...
herbelin
2003-10-08
*
Renommage no-strict en -strict-implicit
herbelin
2003-10-08
*
Renommage no-strict en -strict-implicit
herbelin
2003-10-08
*
Renommage no-strict en -strict-implicit; option -dont-load-proofs
herbelin
2003-10-08
*
Mise en place d'un mecanisme ne chargeant pas les preuves opaques
herbelin
2003-10-08
*
maj
filliatr
2003-10-07
*
Essai de traduction du contraire de 'tacledit bin/coqtop.byte' en 'tac...'
herbelin
2003-10-07
*
Debranchement de l'affichage automatique de Proof par le traducteur (trop com...
herbelin
2003-10-07
*
Inspect saute maintenant les marqueurs invisibles
herbelin
2003-10-07
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
Compatibilite V7 des noms d'hypotheses
herbelin
2003-10-07
*
Pour rendre make un peu moins verbeux
letouzey
2003-10-06
*
NEWCONTRIBVO doit apparaitre apres CONTRIBVO
herbelin
2003-10-06
*
pour ocamlweb
letouzey
2003-10-06
*
distinguer interp_cs et interp_setcs
letouzey
2003-10-06
*
Debranchement de la regle .v.vo pour que celle-ci ne soit pas prise quand new...
herbelin
2003-10-04
[next]