aboutsummaryrefslogtreecommitdiff
path: root/Makefile
AgeCommit message (Collapse)Author
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-24ide changesmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3694 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-13Debugger plus informatifdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3675 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-04interface GTK2 experimentalemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3660 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-03make check utilise toujours le Coq localfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3654 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30Adds a possibility to construct a term as if it had been parsed throughbertot
a user-defined notation, but without actually using the notation. Changes the files needed to construct the parser : file lib/stamps does not seem to be used. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3631 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30Make sure the parser is compiled in native mode.bertot
Make sure the coq-interface.opt binary is compiled in native mode (was wrong in the previous version). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3630 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30Ajoute les directives pour créer aussi bin/coq-interface.optbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3629 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30pas de Xml.vofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3626 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-24on cree toujours le sous-repertoire tactics/filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3609 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-23Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3603 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22removes all references to ctast.ml the Makefile has been updated accordingly.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3591 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22MAJ pour renommage Rcompletdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3579 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-21Binome.v -> Binomial.vdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3561 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16renommage de TAF.v en MVT.vdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3511 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16Renommage de RealsB en Rbasedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3508 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-06bit vectorsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3488 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09setoids dans norealletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3402 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-29MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3342 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27Réorganisation de la librairie des réelsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3312 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27Réorganisation de la librairie des réelsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3311 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Options make coqlight/ make install-coqlight pour les impatients...desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3301 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Option pour compiler une version 'light' des réelsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3299 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3296 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; ↵herbelin
améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3270 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-05Intégration des modifs de la branche mowgli :herbelin
- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-04ajout d'une entrée au makefile pour faire toutes les theories sauf les realsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3205 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-15commit du calcul des dependances un peu plus robustebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3147 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-14*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3143 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ↵herbelin
hack temporaire autour du printer git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3128 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-10Ajout ClassicalFactsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3113 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-07Lazy manuelles dans le codecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3100 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-07Make sure that bin/parser exists when checking that it worksbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3094 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-05Lazy experimentale temporaire...coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-02*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3068 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01Adding the congruence closure tactics (CC and CCsolve).corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3061 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-25*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3033 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-18retablissement de Correctness (pas encore teste' cependant)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3016 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-19Pretty-printing preliminaire des modules, commandescoq
Print Module qid. Print Module Type qid. et affichage pendant Print All. Tout ca est preliminare, seuls les noms des composants sont affiches et non pas les corps... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2973 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-31*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2947 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-31*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2944 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-29*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2931 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-18*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2896 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-17ajout de make otags utilisant otags plutot que etagsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2892 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-17modification de make tags pourletouzey
1) eviter de parser les fichiers de contrib/extraction/test et de depasser les capacitees de etags 2) supprimer les tags ne venant pas des regexps fournis (--language=none) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2891 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16MAJ Makefile pour Realsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2881 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 22:43:23 +0000