index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2003-03-03
fichiers sur la ligne de commande passes a Coq IDE
filliatr
2003-03-03
Retour vieil afficheur
herbelin
2003-03-03
IDE:coloration
filliatr
2003-03-03
IDE: debug=false
filliatr
2003-03-03
coqide: preferences support and optimizations
monate
2003-03-01
Added some tests to make more robust the tactique "Functional
courtieu
2003-02-28
fixing a typo in the new Funinv.v test in test-suite/success
courtieu
2003-02-28
Recuperation des outputs de l'interpretation des commandes vernac et des erre...
desmettr
2003-02-28
maj
filliatr
2003-02-27
coqide updates: copy/paste enhanced. Optimizing coqide on very large inputs. ...
monate
2003-02-27
Interpretation des entiers dans les reels via les scopes
desmettr
2003-02-27
MAJ
herbelin
2003-02-27
Nouvelle syntaxe style 'Inductive color : Set := black, blue, white : color'...
herbelin
2003-02-27
Correction test token normal
herbelin
2003-02-27
1.342 par rapport a 1.340 contourne un bug '-pp camlp4o' (version 1.341 corro...
herbelin
2003-02-27
Contournement bug '-pp camlp4o'
herbelin
2003-02-27
Le lexeur et Notation savent reconnaître si un unicode des blocs
herbelin
2003-02-27
Adding tests for the "functional induction" facility.
bertot
2003-02-27
The contribution of Pierre Courtieu on generating specialized induction schemes
bertot
2003-02-27
Retour nouvel afficheur
herbelin
2003-02-27
Restructuration des hints pour qu'Auto fasse moins de détours et les
herbelin
2003-02-27
maj
filliatr
2003-02-26
Changed Tauto so it displays less 'Unfold not iff'
corbinea
2003-02-26
coqide: preliminary support for mnemonics. Edit menu. Context help now works ...
monate
2003-02-26
maj
filliatr
2003-02-25
ide:copy/paste fix
monate
2003-02-25
Suppression des warnings a la compilation de contrib/linear
corbinea
2003-02-25
maj
filliatr
2003-02-24
coqide : aide sur selection ou sur mot
monate
2003-02-24
Bringing Linear back to life (Still somewhat buggy).
corbinea
2003-02-24
aide contextuelle / menus compilation + print + export
filliatr
2003-02-24
on sait se refaire uniquement si option -f
filliatr
2003-02-24
coq_makefile dit comment faire le .depend (evite l'echec lorsque
filliatr
2003-02-24
False dependencies in summary
coq
2003-02-24
ide changes
monate
2003-02-24
ctrl-k like Emacs in coqide
monate
2003-02-24
ide
monate
2003-02-24
*** empty log message ***
monate
2003-02-22
maj
filliatr
2003-02-21
CoqIDE: robustesse / multi-buffers / menus / ... (utilisable)
filliatr
2003-02-21
bugs/améliorations trouvés via FTA
letouzey
2003-02-17
Affinement entree annot
herbelin
2003-02-15
maj
filliatr
2003-02-14
prise en compte des sous-repertoires Coq de maniere dynamique
filliatr
2003-02-14
Ajout du theoreme de Cesaro
desmettr
2003-02-14
MAJ pour Reals/SeqSeries.v
desmettr
2003-02-13
Test de non bouclage malencontreux dans les niveaux
herbelin
2003-02-13
Modifications dans une tactique toplevel
delahaye
2003-02-13
Correction d'un bug introduit dans le backtracking d'occurrence
delahaye
2003-02-13
Chargement dynamique de .cma
delahaye
[next]