aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-11-21ln -sf au lieu de ln -sfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@907 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21ajout d'un frozen_state après la fermeture d'une section (sinon bug !)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@906 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21implicites manuelsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@905 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21PatternMatchingFailure n'etait pas rattrapeeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@904 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@903 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21Bugs make_tuple et existS_patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@902 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@901 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21ajout de theories/Wellfoundedfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@900 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21Begin-End Silent deviennent Set?Unset Silentmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@899 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21correction bug Resetfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@898 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21separation calcul des implicites et declaration des constantes / inductifs / ↵filliatr
variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@897 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21XML débranchéfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@896 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21Prise en compte des implicites dans les regles de grammairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@895 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Petit bug entre close_section'sherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@894 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Mieux à sa place dans toplevelherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@893 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20La variable argument d'un non-terminal dans Grammar est maintenant un Var ( ↵herbelin
plus un Id ) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@892 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Prise en compte des noms qualifiés dans certaines commandesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@891 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Nouveau lexeme METAIDENT pour les $idherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@890 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Ajout diverses entrées pour les noms qualifiésherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@889 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Ajout implicits_of_global + accès par noms longsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@888 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Tables séparées pour chaque type de globalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@887 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Remplacement des hacks pour les noms longs par un appel à ↵herbelin
Declare.global_qualified_reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@886 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Utilisation de global_reference dans rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@885 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Prise en compte des noms qualifiés dans certaines commandesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@884 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Prise en compte noms longsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@883 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Tables séparées pour chaque type de global; calcul de la Nametab de la ↵herbelin
section; une capsule pour save_module_to git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@882 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Acceptation des noms qualifiés; utilisation de global_reference dans ↵herbelin
pattern; prise en compte des noms qualifiés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@881 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Nouvelle entrée qualidarg pour noms qualifiés; nouveau lexeme METAIDENT ↵herbelin
pour les $id git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@880 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Acceptation des noms qualifiés; nouveau lexeme METAIDENT pour les $idherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@879 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20"Distinction entre . suivi d'un blanc et . suivi d'un ident (pour les noms ↵herbelin
qualifiés; nouveau lexeme METAIDENT pour les \$id' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@878 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@877 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Utilisation de global_reference dans patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@876 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Ajout sp_of_global; Introduction constant_path = section_pathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@875 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Prise en compte camlp4.opt dans la configuration et le Makefileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@874 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Utilisation de global_reference dans rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@873 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Utilisation de global_reference dans rawconstr; blindage pour quand appelé ↵herbelin
du debugger git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@872 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Remplacement des hacks pour les noms longs par un appel à ↵herbelin
Declare.global_qualified_reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@871 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Introduction constant_path = section_pathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@870 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Open est maintenant géré par Nametabherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@869 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Nouveaux points d'accès pour les noms qualifiésherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@868 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Bug dans la règle de syntaxe de ex2herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@867 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Nouvelle structure arborescente à la Nametab pour prendre en compte les ↵herbelin
noms qualifiés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@866 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Prise en compte constructeur QUALID pour noms qualifiésherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@865 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Prise en compte des noms qualifiés dans certaines commandes; nouveau lexeme ↵herbelin
METAIDENT pour les $id; nouvelle entrée pour les noms qualifiés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@864 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Nettoyage + prise en compte noms longsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@863 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Suppression de la section fast_integer qui cachait le nom du module éponymeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@862 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Ajout d'une Nametab et d'un flag export aux ClosedSection; on applique ↵herbelin
export_objet aussi aux sections git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@861 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Ajout erreur GlobalNotFoundherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@860 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Cablage des syntactif defs avec la Nametab des objetsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@859 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Mieux à sa place dans toplevelherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@858 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 10:30:52 +0000