index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
Commit message (
Expand
)
Author
Age
*
MAJ syntaxe
herbelin
2002-11-14
*
typo
courant
2002-11-13
*
rep why ignore
filliatr
2002-11-12
*
Intégration de la branche mowgli
herbelin
2002-11-05
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
cosmetique
letouzey
2002-11-05
*
un bug concernant l'expansion des Map_rec si Map n'est pas ouvert
letouzey
2002-11-04
*
nettoyage et reorganisation
letouzey
2002-11-04
*
maj avec tous les mli
letouzey
2002-11-04
*
Un fichier a utiliser via Drop pour le debug de l'extraction.
letouzey
2002-11-04
*
L'extraction c'est magic cvs -n up
letouzey
2002-10-31
*
Des critères plus fins d'analyse des implicites automatiques; meilleur affic...
herbelin
2002-10-28
*
Clarification changements autour de Remark/Fact/Local
herbelin
2002-10-23
*
Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...
herbelin
2002-10-23
*
Meilleure lisibilité grâce à tclTHENLIST
herbelin
2002-10-19
*
Réparation bug #180
herbelin
2002-10-19
*
TacCall attend une référence
herbelin
2002-10-14
*
Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'une
herbelin
2002-10-14
*
Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...
herbelin
2002-10-13
*
Lazy manuelles dans le code
coq
2002-10-07
*
correcting the treatment of many tactics that use quant_hyp in file xlate.ml
bertot
2002-10-06
*
Lazy experimentale temporaire...
coq
2002-10-05
*
Re-introduce the treatement of Tacticals that Hugo had already done in
bertot
2002-10-04
*
Previous version did compile but did not make it possible to actually run
bertot
2002-10-03
*
Omega can now elim hyps of type False. Therefore, it knows how to deal
courant
2002-10-02
*
Adding the congruence closure tactics (CC and CCsolve).
corbinea
2002-10-01
*
Complétion filtrage
herbelin
2002-09-29
*
Un peu (plus) d'ordre dans Nametab...
coq
2002-09-24
*
suite chgt liés aux modules
letouzey
2002-09-24
*
portage Correctness (substitutivité pour les modules)
filliatr
2002-09-19
*
retablissement de Correctness (pas encore teste' cependant)
filliatr
2002-09-18
*
Suppression automatique du corps des définitions locales opaques dans
herbelin
2002-08-17
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
reparation d'un bug (dummy_lams -> anonym_lams) + chgmt structutr d'un ml_type
letouzey
2002-07-24
*
reparation temporaire(?) a coup de MLdummy'
letouzey
2002-07-17
*
maj
letouzey
2002-07-16
*
Pour ocamlweb
letouzey
2002-07-16
*
Souci avec example fbidon...
letouzey
2002-07-16
*
petit bug lors du passage d'hugo
letouzey
2002-07-16
*
Gros Remaniement Extraction:
letouzey
2002-07-16
*
Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour
herbelin
2002-07-11
*
Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulement
filliatr
2002-06-21
*
ZArith_base, Zbool, Bool_nat
filliatr
2002-06-20
*
Reparation de ring pour les setoides
clrenard
2002-06-19
*
ProgWf -> Zwf
filliatr
2002-06-19
*
deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwf
filliatr
2002-06-19
*
extraction vers scheme
letouzey
2002-06-07
*
Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...
herbelin
2002-06-05
*
Intgration uniforme de coercions dans les dclarations (Variable and co) et re...
herbelin
2002-06-03
*
Protection des tactiques contre l'utilisation sans le bon contexte de thories
herbelin
2002-06-03
[next]