aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-11-23Informations inutilesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@925 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp;herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@924 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@923 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Ajout push_rels_assumherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@922 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Bug qualidconstarg (intervient pour Transparent)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@921 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Reparation IsMutConstruct + Transparentmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@920 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de ↵herbelin
'section_path' pour les noms absolus git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@918 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22deplacement poly_args; iterateurs sur les segmentsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@917 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22Reparation bug mutuels indmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@916 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22retablissement de line_oriented_parser pour Yvesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@915 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22des proofs/macros qui trainaient dans le Makefile et le .dependfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@914 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21Tout est deja traite dans Tacinterpdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@913 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21Elimination d'un test sur les macrosdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@912 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21Traitement du pretty-print des Redexpdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@911 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21Ajout d'une fonction pour recuperer la liste des constantesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@910 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21Ajout du clean pour tolink.mldelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@909 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21reset_name: try / with juste autour de find_entry_p (=> propage lesfilliatr
vraies erreurs de reset_to s'il y en a) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@908 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-18 18:08:20 +0000