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
*
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
*
Suppression des explicitations d'implicite inutiles
herbelin
2003-04-07
*
Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun implicite
herbelin
2003-04-07
*
Options d'affichage maintenant dans Constrextern
herbelin
2003-04-07
*
Options d'affichage maintenant dans Constrextern
herbelin
2003-04-07
*
maj
filliatr
2003-04-04
*
Documentation, généralisation à eq sur Type, preuves d'équivalence des
herbelin
2003-04-03
*
Backtrack du commit de Christine, qui posait probleme avec FTC
letouzey
2003-04-03
*
Légères simplifications code de Field; message d'erreur si pas égalité
herbelin
2003-04-03
*
maj
filliatr
2003-04-03
*
espace manquant
herbelin
2003-04-02
*
remplace == par = dans la tactique field pour que le debugger marche a nouvea...
narboux
2003-04-01
*
maj
filliatr
2003-04-01
*
Déplacement with_option dans Options
herbelin
2003-04-01
*
Correction bug #261 + amélioration nommage
herbelin
2003-04-01
*
Extension de Replace aux égalités entre preuves
herbelin
2003-04-01
*
Fail 1 pour traverser le match
herbelin
2003-04-01
*
maj
filliatr
2003-04-01
*
MAJ
herbelin
2003-03-31
*
Noms absolus
herbelin
2003-03-31
*
Ajout double_plus
herbelin
2003-03-31
*
Ajout Implicit Variable Type
herbelin
2003-03-31
[next]