aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
Commit message (Collapse)AuthorAge
* Module Bij inutiliseGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4129 85f007b7-540e-0410-9357-904b9bb8a0f7
* au lieu de makeGravatar monate2003-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4095 85f007b7-540e-0410-9357-904b9bb8a0f7
* moved engine.ml4 to ground.ml4, added option 'Ground Depth'Gravatar corbinea2003-05-26
| | | | | | | fixed utf8.vo dependency. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4078 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: blaster 2Gravatar monate2003-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4071 85f007b7-540e-0410-9357-904b9bb8a0f7
* fabrication de ide/utf8.voGravatar letouzey2003-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4070 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: blaster V1Gravatar monate2003-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4059 85f007b7-540e-0410-9357-904b9bb8a0f7
* Concentration des notations officielles dans Init/Notations; restructuration ↵Gravatar herbelin2003-05-21
| | | | | | de Init git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4050 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructutation Hipattern PatternGravatar herbelin2003-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4034 85f007b7-540e-0410-9357-904b9bb8a0f7
* configure et make install s'occupent de CoqIde tout seulsGravatar filliatr2003-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4029 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: .* on start/add \n on eofGravatar monate2003-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4022 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: load/save file encoding support/Gravatar monate2003-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4021 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux lemmes (sur proposition de Nijmegen)Gravatar herbelin2003-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4012 85f007b7-540e-0410-9357-904b9bb8a0f7
* entréé translation2Gravatar herbelin2003-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3990 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout ChoiceFactsGravatar herbelin2003-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3977 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: search forwardGravatar monate2003-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3969 85f007b7-540e-0410-9357-904b9bb8a0f7
* fichier de pref coq IDE en ASCII (ENFIN)Gravatar filliatr2003-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3963 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added the Ground tactic.Gravatar corbinea2003-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3955 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout "at next level" dans NotationGravatar herbelin2003-04-17
| | | | | | | Mise en place structure pour définir un objet en même temps que sa notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3939 85f007b7-540e-0410-9357-904b9bb8a0f7
* BIG MAJ Extraction:Gravatar letouzey2003-04-16
| | | | | | | | | | | | | | | | | ------------------ - (Recursive) Extraction Module devient (Recursive) Extraction Library (pour cause d'ambiguite avec les nouveaux modules Coq). - un nouveau Extraction Module qui extrait dans le toplevel tout module Coq - tout fixpoint est de nouveau inlinable (Yves). - fix bug du calcul d'env minimal des modules en extraction monolithique. - un nouveau fichier Modutil regroupant manques de Modops & functions specifiques aux modules MiniML - plus d'aliases a trainer (mais des substitutions des le depart) - ET SURTOUT: un nommage correct (ou du moins moins pire) dans les modtypes et les functors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3934 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: thread bug fixGravatar monate2003-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3900 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide : introduction des coprocessus. CoqIde est maintenant interruptibleGravatar monate2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3887 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option -v8 à coqtopnew pour permettre le changement de comportement ↵Gravatar herbelin2003-04-09
| | | | | | des implicites (passage au mode strict) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3882 85f007b7-540e-0410-9357-904b9bb8a0f7
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
| | | | | | | | | pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3858 85f007b7-540e-0410-9357-904b9bb8a0f7
* BEST redondantGravatar herbelin2003-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3849 85f007b7-540e-0410-9357-904b9bb8a0f7
* remplace == par = dans la tactique field pour que le debugger marche a ↵Gravatar narboux2003-04-01
| | | | | | nouveau apres suppression de == par hugo git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3837 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)Gravatar herbelin2003-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3806 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqmktop: -ide fait ce qu'il faut (on peut maintenant construire des Coq IDE ↵Gravatar filliatr2003-03-17
| | | | | | customises) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3778 85f007b7-540e-0410-9357-904b9bb8a0f7
* nettoyage dans translateGravatar filliatr2003-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3777 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: maj preferences du wizzardGravatar monate2003-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3774 85f007b7-540e-0410-9357-904b9bb8a0f7
* nettoyage dans ide/utilsGravatar filliatr2003-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3772 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3771 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparations suite a la nouvelle syntaxe:Gravatar barras2003-03-14
| | | | | | | | - syntaxe des modules - syntaxe existentielle git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3769 85f007b7-540e-0410-9357-904b9bb8a0f7
* petites erreursGravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3762 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Ajout du traducteur nouvelle syntaxe *Gravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3760 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: fenetre de cmmandes . undo correctGravatar monate2003-03-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3747 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: le undoGravatar monate2003-03-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3746 85f007b7-540e-0410-9357-904b9bb8a0f7
* IDE: menu templatesGravatar filliatr2003-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3742 85f007b7-540e-0410-9357-904b9bb8a0f7
* install de coq.pngGravatar marche2003-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3738 85f007b7-540e-0410-9357-904b9bb8a0f7
* fichiers sur la ligne de commande passes a Coq IDEGravatar filliatr2003-03-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3728 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: preferences support and optimizationsGravatar monate2003-03-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3724 85f007b7-540e-0410-9357-904b9bb8a0f7
* 1.342 par rapport a 1.340 contourne un bug '-pp camlp4o' (version 1.341 ↵Gravatar herbelin2003-02-27
| | | | | | corrompue) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3714 85f007b7-540e-0410-9357-904b9bb8a0f7
* Contournement bug '-pp camlp4o'Gravatar herbelin2003-02-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3713 85f007b7-540e-0410-9357-904b9bb8a0f7
* The contribution of Pierre Courtieu on generating specialized induction schemesGravatar bertot2003-02-27
| | | | | | | for recursive functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3710 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bringing Linear back to life (Still somewhat buggy).Gravatar corbinea2003-02-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3699 85f007b7-540e-0410-9357-904b9bb8a0f7
* aide contextuelle / menus compilation + print + exportGravatar filliatr2003-02-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3698 85f007b7-540e-0410-9357-904b9bb8a0f7
* ide changesGravatar monate2003-02-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3694 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: robustesse / multi-buffers / menus / ... (utilisable)Gravatar filliatr2003-02-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3689 85f007b7-540e-0410-9357-904b9bb8a0f7
* Debugger plus informatifGravatar delahaye2003-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3675 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du traducteurGravatar desmettr2003-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3664 85f007b7-540e-0410-9357-904b9bb8a0f7
* interface GTK2 experimentaleGravatar monate2003-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3660 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 12:24:45 +0000