aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-03-03fichiers sur la ligne de commande passes a Coq IDEfilliatr
2003-03-03Retour vieil afficheurherbelin
2003-03-03IDE:colorationfilliatr
2003-03-03IDE: debug=falsefilliatr
2003-03-03coqide: preferences support and optimizationsmonate
2003-03-01Added some tests to make more robust the tactique "Functionalcourtieu
2003-02-28fixing a typo in the new Funinv.v test in test-suite/successcourtieu
2003-02-28Recuperation des outputs de l'interpretation des commandes vernac et des erre...desmettr
2003-02-28majfilliatr
2003-02-27coqide updates: copy/paste enhanced. Optimizing coqide on very large inputs. ...monate
2003-02-27Interpretation des entiers dans les reels via les scopesdesmettr
2003-02-27MAJherbelin
2003-02-27Nouvelle syntaxe style 'Inductive color : Set := black, blue, white : color'...herbelin
2003-02-27Correction test token normalherbelin
2003-02-271.342 par rapport a 1.340 contourne un bug '-pp camlp4o' (version 1.341 corro...herbelin
2003-02-27Contournement bug '-pp camlp4o'herbelin
2003-02-27Le lexeur et Notation savent reconnaître si un unicode des blocsherbelin
2003-02-27Adding tests for the "functional induction" facility.bertot
2003-02-27The contribution of Pierre Courtieu on generating specialized induction schemesbertot
2003-02-27Retour nouvel afficheurherbelin
2003-02-27Restructuration des hints pour qu'Auto fasse moins de détours et lesherbelin
2003-02-27majfilliatr
2003-02-26Changed Tauto so it displays less 'Unfold not iff'corbinea
2003-02-26coqide: preliminary support for mnemonics. Edit menu. Context help now works ...monate
2003-02-26majfilliatr
2003-02-25ide:copy/paste fixmonate
2003-02-25Suppression des warnings a la compilation de contrib/linearcorbinea
2003-02-25majfilliatr
2003-02-24coqide : aide sur selection ou sur motmonate
2003-02-24Bringing Linear back to life (Still somewhat buggy).corbinea
2003-02-24aide contextuelle / menus compilation + print + exportfilliatr
2003-02-24on sait se refaire uniquement si option -ffilliatr
2003-02-24coq_makefile dit comment faire le .depend (evite l'echec lorsquefilliatr
2003-02-24False dependencies in summarycoq
2003-02-24ide changesmonate
2003-02-24ctrl-k like Emacs in coqidemonate
2003-02-24idemonate
2003-02-24*** empty log message ***monate
2003-02-22majfilliatr
2003-02-21CoqIDE: robustesse / multi-buffers / menus / ... (utilisable)filliatr
2003-02-21bugs/améliorations trouvés via FTAletouzey
2003-02-17Affinement entree annotherbelin
2003-02-15majfilliatr
2003-02-14prise en compte des sous-repertoires Coq de maniere dynamiquefilliatr
2003-02-14Ajout du theoreme de Cesarodesmettr
2003-02-14MAJ pour Reals/SeqSeries.vdesmettr
2003-02-13Test de non bouclage malencontreux dans les niveauxherbelin
2003-02-13Modifications dans une tactique topleveldelahaye
2003-02-13Correction d'un bug introduit dans le backtracking d'occurrencedelahaye
2003-02-13Chargement dynamique de .cmadelahaye