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
*
maj
filliatr
2003-04-10
*
cast de nil
herbelin
2003-04-09
*
Affichage des inductifs
herbelin
2003-04-09
*
nil en implicite dans la v8
herbelin
2003-04-09
*
Bug init_function
herbelin
2003-04-09
*
Synchronisation séparée des implicites pour l'affichage du traducteur;
herbelin
2003-04-09
*
Formattage affichage
herbelin
2003-04-09
*
Correction Show Implicits
herbelin
2003-04-09
*
Ajout Open Scope
herbelin
2003-04-09
*
Mécanisme plus simple et efficace pour traduire les implicites
herbelin
2003-04-09
*
Gestion synchronisation des Impargs.*_out et des Impargs._strict dans Impargs
herbelin
2003-04-09
*
Coqide : introduction des coprocessus. CoqIde est maintenant interruptible
monate
2003-04-09
*
Activation des implicites pour la v8
herbelin
2003-04-09
*
MAJ
herbelin
2003-04-09
*
Bugs synchronisation pour gestion traduction des implicites
herbelin
2003-04-09
*
Synchronisation avec reset
herbelin
2003-04-09
*
Ajout option -v8 à coqtopnew pour permettre le changement de comportement de...
herbelin
2003-04-09
*
Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"
herbelin
2003-04-09
*
Alignement du comportement des implicites d'inductif en sortie de section sur...
herbelin
2003-04-09
*
Renommage K; equivalence JMeq et eq_dep sur Type
herbelin
2003-04-09
*
Defined
herbelin
2003-04-09
*
Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".
herbelin
2003-04-09
*
Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"
herbelin
2003-04-09
*
Réorganisation de Impargs + mise en place d'une infrastructure
herbelin
2003-04-09
*
Réorganisation de Impargs + mise en place d'une infrastructure
herbelin
2003-04-09
*
Prise en compte affichage coercions traducteur dans Constrextern
herbelin
2003-04-09
*
on repasse aussi -thread a Caml
filliatr
2003-04-08
*
test: un boolean et une fonction check_for_interrupt inseree dans la conversi...
filliatr
2003-04-08
*
Prise en compte des variables de grammaires de tactiques et dédollarisation ...
herbelin
2003-04-08
*
Application de l'absence d'export aux modules
herbelin
2003-04-08
*
En-tete doc
herbelin
2003-04-08
*
Ajout option "Local" à "Open Scope"
herbelin
2003-04-08
*
maj
filliatr
2003-04-08
*
Affichage des tactiques en v8
herbelin
2003-04-07
*
lconstr pour genterm en v8
herbelin
2003-04-07
*
Ajout translate
herbelin
2003-04-07
*
Typo
herbelin
2003-04-07
*
Nommage explicite des hypotheses introduites quand le nom existe aussi comme ...
herbelin
2003-04-07
*
Globalisation tactiques
herbelin
2003-04-07
*
Mauvaise resolution conflit dans commit precedent
herbelin
2003-04-07
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Stratégie d'affichage des coercions plus défensive (mais pas très optimale)
herbelin
2003-04-07
*
Cosmetique
herbelin
2003-04-07
*
code mort
herbelin
2003-04-07
*
Espaces superflus
herbelin
2003-04-07
*
Renommage unicite/unicity pour la v8
herbelin
2003-04-07
*
Aérer les := et : de "assert"
herbelin
2003-04-07
*
Ajout cas Match
herbelin
2003-04-07
*
BEST redondant
herbelin
2003-04-07
[next]