aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2003-02-05Ajout du traducteurdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3664 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-05Suppression de l'élimination des existentiels dans LinearIntuition.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3663 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-05Automatisation de la création de l'image avec le package MacOS-Xherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3662 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-05majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3661 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-04interface GTK2 experimentalemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3660 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-04MAJ Windowsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3659 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-04MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3658 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-04Contournement de ocamlmktop qui plante sous win32herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3657 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-11 00:13:22 +0000