aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-02-27coqide updates: copy/paste enhanced. Optimizing coqide on very large inputs. ↵monate
Contextual colorization. Synchronization problems solved. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3719 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27Interpretation des entiers dans les reels via les scopesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3718 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3717 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27Nouvelle syntaxe style 'Inductive color : Set := black, blue, white : ↵herbelin
color' pour les types énumérés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3716 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27Correction test token normalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3715 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-271.342 par rapport a 1.340 contourne un bug '-pp camlp4o' (version 1.341 ↵herbelin
corrompue) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3714 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27Contournement bug '-pp camlp4o'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3713 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27Le lexeur et Notation savent reconnaître si un unicode des blocsherbelin
0380-03FF (lettres grecques) 2100-214F (symboles assimilés à des lettres), 2200-22FF (opérateurs mathématiques), 2300-23FF (symboles techniques divers) et 2600-26FF (symboles divers) est un caractère spécial ou non lorsque encodé en utf-8. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3712 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27Adding tests for the "functional induction" facility.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3711 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27The contribution of Pierre Courtieu on generating specialized induction schemesbertot
for recursive functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3710 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27Retour nouvel afficheurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3709 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27Restructuration des hints pour qu'Auto fasse moins de détours et lesherbelin
preuves soient plus naturelles. En particulier, tentative de ramener systématiquement > et >= vers < et <=. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3708 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3707 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-26Changed Tauto so it displays less 'Unfold not iff'corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3706 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-26coqide: preliminary support for mnemonics. Edit menu. Context help now works ↵monate
properly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3705 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-26majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3704 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-25ide:copy/paste fixmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3703 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-25Suppression des warnings a la compilation de contrib/linearcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3702 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-25majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3701 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-24coqide : aide sur selection ou sur motmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3700 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-24Bringing Linear back to life (Still somewhat buggy).corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3699 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-24aide contextuelle / menus compilation + print + exportfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3698 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-24on sait se refaire uniquement si option -ffilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3697 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-24coq_makefile dit comment faire le .depend (evite l'echec lorsquefilliatr
.depend n'existe pas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3696 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-24False dependencies in summarycoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3695 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-24ide changesmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3694 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-24ctrl-k like Emacs in coqidemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3693 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-24idemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3692 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-24*** empty log message ***monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3691 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3690 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-21CoqIDE: robustesse / multi-buffers / menus / ... (utilisable)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3689 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-21bugs/améliorations trouvés via FTAletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3688 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-17Affinement entree annotherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3687 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-15majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3683 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-14prise en compte des sous-repertoires Coq de maniere dynamiquefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3682 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-14Ajout du theoreme de Cesarodesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3681 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-14MAJ pour Reals/SeqSeries.vdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3680 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-13Test de non bouclage malencontreux dans les niveauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3679 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-13Modifications dans une tactique topleveldelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3678 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-13Correction d'un bug introduit dans le backtracking d'occurrencedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3677 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-13Chargement dynamique de .cmadelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3676 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-13Debugger plus informatifdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3675 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-12majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3674 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-11Undo dans Coq IDEfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3673 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-08Bug Renameherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3671 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-08Bug Renameherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3670 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-06MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3668 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-06commentairecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3667 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-06majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3666 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-05updatedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3665 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-20 04:23:52 +0000