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
*
Distinction mode v7 ou translate; conséquences du déplacement traducteur de...
herbelin
2003-06-10
*
Déplacement de code dans command; MAJ DebugOn
herbelin
2003-06-10
*
Mise en place structure pour des 'arguments scope' dirigés par une classe
herbelin
2003-06-10
*
Amélioration afficheur de Cases pour les constr_pattern
herbelin
2003-06-10
*
Passage des noms de tactiques à kernel_name pour compatibilité avec les fon...
herbelin
2003-06-10
*
Déplacement traducteur de nom dans Constrextern pour accès aux noms longs
herbelin
2003-06-10
*
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2003-06-10
*
Factorisation de detype_case pour utilisation par l'afficheur de pattern
herbelin
2003-06-10
*
Traducteur + passage des noms de tactiques à kernel_name pour compatibilité...
herbelin
2003-06-10
*
Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...
herbelin
2003-06-10
*
Amélioration afficheur de Cases pour les constr_pattern
herbelin
2003-06-10
*
Extension de Locate sur les symboles avec recherche de sous-chaînes; mise en...
herbelin
2003-06-10
*
Globalisation de ce qui n'etait pas encore globalise
herbelin
2003-06-10
*
code mort
herbelin
2003-06-10
*
Ajout fonctions de recherche de sous-chaines (merci a Jacek)
herbelin
2003-06-10
*
maj
filliatr
2003-06-09
*
interaction entre fun/case permut et assert false
letouzey
2003-06-08
*
Tables logarithmiques pour les coercions + nettoyage
herbelin
2003-06-08
*
coqide: compile sans activate repare
monate
2003-06-06
*
bug CoqIDE avec Goal
filliatr
2003-06-06
*
Added new syntax definition
barras
2003-06-06
*
bugfix for Ground ( merci JC )
corbinea
2003-06-04
*
Ground update + some bugfix
corbinea
2003-06-04
*
au lieu de make
monate
2003-06-02
*
oups
letouzey
2003-05-30
*
maj
filliatr
2003-05-30
*
Bug niveau
herbelin
2003-05-29
*
niveau 49 devient next
herbelin
2003-05-29
*
Ground daily update
corbinea
2003-05-29
*
niveau 49 devient next
herbelin
2003-05-29
*
Ne pas mettre d'associatif a droite au niveau 3 en V7
herbelin
2003-05-29
*
:= dans un record engendre un LetIn qui n'etait pas géré
letouzey
2003-05-29
*
gestion plus fine des beta-redex lineaires (cf nb_occur_match)
letouzey
2003-05-28
*
'only parsing' pour le passage de trucT a truc
herbelin
2003-05-27
*
maj
filliatr
2003-05-27
*
coqide: blaster interruptible
monate
2003-05-26
*
Bug
herbelin
2003-05-26
*
GIntuition now matches Intuition up to hyps renaming.
corbinea
2003-05-26
*
Added breakpoint in Ground tactic.
corbinea
2003-05-26
*
moved engine.ml4 to ground.ml4, added option 'Ground Depth'
corbinea
2003-05-26
*
*** empty log message ***
monate
2003-05-26
*
configure pour CoqIde repare
monate
2003-05-26
*
Ground and CCsolve updates
corbinea
2003-05-25
*
"INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans Reals
herbelin
2003-05-24
*
Amélioration affichage locations; prise en compte variables dans lettac; ajo...
herbelin
2003-05-24
*
Ajout FreshId
herbelin
2003-05-24
*
coqide: blaster 2
monate
2003-05-23
*
fabrication de ide/utf8.vo
letouzey
2003-05-23
*
Bug en mode translate
herbelin
2003-05-23
*
maj
filliatr
2003-05-23
[next]