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
*
Extraction des Record, suite
letouzey
2002-11-27
*
Remplacement Grammar/Syntax par Notation
herbelin
2002-11-26
*
Remplacement des Grammar et des [| |] par des notations
herbelin
2002-11-26
*
debut de support des records caml
letouzey
2002-11-26
*
correction bug n°191
letouzey
2002-11-25
*
cleanup table.ml + erreur si Extraction Inline sous section
letouzey
2002-11-25
*
Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...
herbelin
2002-11-24
*
Remplacement de Syntactic Definition par Notation
herbelin
2002-11-24
*
Nettoyage
herbelin
2002-11-24
*
remaniement de test_extraction.v
letouzey
2002-11-18
*
typo
herbelin
2002-11-18
*
Complétion du commit précédent
herbelin
2002-11-16
*
Passage à une représentation des fixpoints plus primitive dans constr_expr ...
herbelin
2002-11-15
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
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
[next]