aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-03-04coqide: bugfixmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3739 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-04install de coq.pngmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3738 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-04belle image de coq (en png en plus)marche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3737 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-04coqide: partage -debug avec coqtopmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3736 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-04tous les fichiers passes a Coq IDEfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3735 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-04IDE: majmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3734 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-04Bug délimiteur de scope en vieil affichage astherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3732 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-04MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3731 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-04majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3730 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-03CoqIDE: copy/pastemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3729 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-03fichiers sur la ligne de commande passes a Coq IDEfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3728 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-03Retour vieil afficheurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3727 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-03IDE:colorationfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3726 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-03IDE: debug=falsefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3725 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-03coqide: preferences support and optimizationsmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3724 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-01Added some tests to make more robust the tactique "Functionalcourtieu
Induction". Namely: check that the given function is a really a constant, and check that the number of given argument is exactly the arity of the given function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3723 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-28fixing a typo in the new Funinv.v test in test-suite/successcourtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3722 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-28Recuperation des outputs de l'interpretation des commandes vernac et des ↵desmettr
erreurs pour le traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3721 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3720 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 15:16:43 +0000