aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2003-11-26Export string_index_fromherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4997 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Marge presqu'a 80, maximum indentation a 50 pour une meilleure lisibiliteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4658 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Ajout projections de tripletherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4625 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11reparation Undo suiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4603 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Bug undoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4587 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Gestion en temps constant de la pile des Unfoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4560 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
extraction: pb avec les variables de section definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4450 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22Passage à la V8 par défautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4437 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-14Bug PR#324herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4398 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et ↵herbelin
choix du parseur en fonction de cette option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4387 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10warning vers std_errherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4346 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Positionnement precoce de l'option -v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4270 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Option -v8 à coqtop lance coqtopnew; option -no-strict; option -no-proofsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4254 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-10Ajout option_fold_rightherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4251 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-12Ajout option translate_syntax pour caractériser l'interprétation du ↵herbelin
traducteur à proprement parler git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4139 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Module Bij inutiliseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4133 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Ajout fonctions de recherche de sous-chaines (merci a Jacek)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4106 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29Mise en place d'un 2ème traducteur à l'essai (activable avec -ftranslate2)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3981 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29Ajout is_ident_tailherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3970 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-25Added the Ground tactic.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3955 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-16une fonction list_skipn qui zappe les n premiers elements d'une listeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3930 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-08test: un boolean et une fonction check_for_interrupt inseree dans la ↵filliatr
conversion pour permettre a Coq IDE d'interrompre Coq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3871 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-01Déplacement with_option dans Optionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3835 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-26Ajout de Set Print Widthgregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3790 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-21*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3783 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 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
2002-12-10Ajout options -v7 et -v8, et commandes V7only et V8onlyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3410 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-10Ajout options -v7 et -v8, et commandes V7only et V8onlyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3407 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Take notations into account: numbers and the CNotation operator.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3401 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28A usage cosmetiqueletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3320 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Ajout list_map_assocherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3289 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Ajout option_consherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3265 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Ajout zeroherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3264 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-20Ajout option_fold_left2herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3258 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-05Nouvelle option -xml à coqtop pour compiler un développement enherbelin
l'exportant au format xml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3211 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-14Ajout optino_iterherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3136 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-13Bug affichage du chiffre 0herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3130 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@3120 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-05Lazy experimentale temporaire...coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 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-09-16Réintroduction de l'expansion des variables de shell et de '~' dans lesherbelin
chemins de fichiers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3012 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-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-27Changement Filename.is_relative en Filename.is_implicit, plus pertinentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2710 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-10Amélioration des messages d'erreurs concernant l'inférence des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2630 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:20:54 +0000