aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-04-10Open Scope remplace Importherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3912 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Calcul automatique de l'implicite de nil pour que l'affichage sache le traiterherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3911 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Affichage forcé des implicites contextuels si pas de contexte connuherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3910 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Remplacement Import par Open Scope en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3909 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Suppression de quelques espaces superflusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3908 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Relachement globalisation Unfold en usage interactifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3907 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10coqide: undo fixmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3906 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10*** empty log message ***monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3905 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10*** empty log message ***monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3904 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10coqide: bug highlight corrigemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3903 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10coqide: completion supportmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3902 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10set_focusmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3901 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10coqide: thread bug fixmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3900 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Trop de restriction pour les TacDefherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3899 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3898 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09cast de nilherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3897 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Affichage des inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3896 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09nil en implicite dans la v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3895 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Bug init_functionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3894 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Synchronisation séparée des implicites pour l'affichage du traducteur;herbelin
différentiation aussi pour les Implicites manuels; nettoyage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3893 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Formattage affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3892 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Correction Show Implicitsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3891 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Ajout Open Scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3890 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Mécanisme plus simple et efficace pour traduire les implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3889 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Gestion synchronisation des Impargs.*_out et des Impargs._strict dans Impargsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3888 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Coqide : introduction des coprocessus. CoqIde est maintenant interruptiblemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3887 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Activation des implicites pour la v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3886 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3885 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Bugs synchronisation pour gestion traduction des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3884 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Synchronisation avec resetherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3883 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Ajout option -v8 à coqtopnew pour permettre le changement de comportement ↵herbelin
des implicites (passage au mode strict) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3882 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3881 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Alignement du comportement des implicites d'inductif en sortie de section ↵herbelin
sur celui des constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3880 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Renommage K; equivalence JMeq et eq_dep sur Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3879 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Definedherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3878 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3877 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
Expérience avec les notations et les scopes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3876 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Réorganisation de Impargs + mise en place d'une infrastructureherbelin
(notatemment des tables de parsing et d'affichage différenciées) permettant au traducteur de changer les implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3875 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Réorganisation de Impargs + mise en place d'une infrastructureherbelin
(notatemment des tables de parsing et d'affichage différenciées) permettant au traducteur de changer les implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3874 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Prise en compte affichage coercions traducteur dans Constrexternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3873 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-08on repasse aussi -thread a Camlfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3872 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-08Prise en compte des variables de grammaires de tactiques et dédollarisation ↵herbelin
des metaident git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3870 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-08Application de l'absence d'export aux modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3869 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-08En-tete docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3868 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-08Ajout option "Local" à "Open Scope"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3867 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-08majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3866 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Affichage des tactiques en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3865 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07lconstr pour genterm en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3864 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Ajout translateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3863 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 16:25:28 +0000