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
*
Ground update
corbinea
2003-06-22
*
Ground update
corbinea
2003-06-20
*
Ground Update.
corbinea
2003-06-20
*
Ajout 'Symmetry in Hyp'
herbelin
2003-06-19
*
Ground update
corbinea
2003-06-16
*
ground update
corbinea
2003-06-16
*
Ground major update ... mmm, sounds exciting !
corbinea
2003-06-15
*
ground update
corbinea
2003-06-14
*
Major Ground update, may break semantics
corbinea
2003-06-14
*
Ajout option Local à Hint, Hints et HintDestruct
herbelin
2003-06-14
*
Ground update
corbinea
2003-06-13
*
Ground update, new files.
corbinea
2003-06-13
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
Ground update.
corbinea
2003-06-13
*
enieme correction du nommage modulaire
letouzey
2003-06-12
*
fin de l'affichage des signatures de modules dans les *.ml
letouzey
2003-06-12
*
Typo
herbelin
2003-06-10
*
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2003-06-10
*
Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...
herbelin
2003-06-10
*
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2003-06-10
*
Globalisation de ce qui n'etait pas encore globalise
herbelin
2003-06-10
*
interaction entre fun/case permut et assert false
letouzey
2003-06-08
*
bugfix for Ground ( merci JC )
corbinea
2003-06-04
*
Ground update + some bugfix
corbinea
2003-06-04
*
oups
letouzey
2003-05-30
*
Ground daily update
corbinea
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
*
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
*
Ground and CCsolve updates
corbinea
2003-05-25
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Mise en conformite de la precedence du '-' unaire avec celle de Notations (su...
herbelin
2003-05-21
*
Mise en conformite de la precedence du '-' unaire avec celle de Notations
herbelin
2003-05-21
*
Mise en conformite de la precedence du '-' unaire avec celle de Notations
herbelin
2003-05-21
*
Concentration des notations officielles dans Init/Notations; restructuration ...
herbelin
2003-05-21
*
MAJ
herbelin
2003-05-21
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Major Ground tactic update, sensible performance improvement
corbinea
2003-05-16
*
Notations arithmetiques
herbelin
2003-05-13
*
bugfixes in Ground.
corbinea
2003-05-08
*
Enhancement of the Ground tactic, addition of GTauto and GIntuition.
corbinea
2003-05-07
*
Localisation erreurs TacAlias; Globalisation moins tolérante dans les
herbelin
2003-04-28
*
bug concernant les projecteurs de Record avec args logiques
letouzey
2003-04-28
*
adaptation a Acc_iter
letouzey
2003-04-28
*
bugfix in Ground tactic
corbinea
2003-04-26
*
Added the Ground tactic.
corbinea
2003-04-25
*
Divers
herbelin
2003-04-17
[next]