aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* Informations inutilesGravatar herbelin2000-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@925 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp;Gravatar herbelin2000-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@924 85f007b7-540e-0410-9357-904b9bb8a0f7
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@923 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout push_rels_assumGravatar herbelin2000-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@922 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug qualidconstarg (intervient pour Transparent)Gravatar herbelin2000-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@921 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation IsMutConstruct + TransparentGravatar mohring2000-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de ↵Gravatar herbelin2000-11-22
| | | | | | 'section_path' pour les noms absolus git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
* NettoyageGravatar herbelin2000-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@918 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacement poly_args; iterateurs sur les segmentsGravatar filliatr2000-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@917 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation bug mutuels indGravatar mohring2000-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@916 85f007b7-540e-0410-9357-904b9bb8a0f7
* retablissement de line_oriented_parser pour YvesGravatar filliatr2000-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@915 85f007b7-540e-0410-9357-904b9bb8a0f7
* des proofs/macros qui trainaient dans le Makefile et le .dependGravatar filliatr2000-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@914 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tout est deja traite dans TacinterpGravatar delahaye2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@913 85f007b7-540e-0410-9357-904b9bb8a0f7
* Elimination d'un test sur les macrosGravatar delahaye2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@912 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traitement du pretty-print des RedexpGravatar delahaye2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@911 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une fonction pour recuperer la liste des constantesGravatar delahaye2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@910 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du clean pour tolink.mlGravatar delahaye2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@909 85f007b7-540e-0410-9357-904b9bb8a0f7
* reset_name: try / with juste autour de find_entry_p (=> propage lesGravatar filliatr2000-11-21
| | | | | | | 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
* ln -sf au lieu de ln -sGravatar filliatr2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@907 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout d'un frozen_state après la fermeture d'une section (sinon bug !)Gravatar filliatr2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@906 85f007b7-540e-0410-9357-904b9bb8a0f7
* implicites manuelsGravatar filliatr2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@905 85f007b7-540e-0410-9357-904b9bb8a0f7
* PatternMatchingFailure n'etait pas rattrapeeGravatar herbelin2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@904 85f007b7-540e-0410-9357-904b9bb8a0f7
* NettoyageGravatar herbelin2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@903 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs make_tuple et existS_patternGravatar herbelin2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@902 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@901 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de theories/WellfoundedGravatar filliatr2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@900 85f007b7-540e-0410-9357-904b9bb8a0f7
* Begin-End Silent deviennent Set?Unset SilentGravatar mohring2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@899 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction bug ResetGravatar filliatr2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@898 85f007b7-540e-0410-9357-904b9bb8a0f7
* separation calcul des implicites et declaration des constantes / inductifs / ↵Gravatar filliatr2000-11-21
| | | | | | variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@897 85f007b7-540e-0410-9357-904b9bb8a0f7
* XML débranchéGravatar filliatr2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@896 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des implicites dans les regles de grammairesGravatar herbelin2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@895 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit bug entre close_section'sGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@894 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mieux à sa place dans toplevelGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@893 85f007b7-540e-0410-9357-904b9bb8a0f7
* La variable argument d'un non-terminal dans Grammar est maintenant un Var ( ↵Gravatar herbelin2000-11-20
| | | | | | plus un Id ) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des noms qualifiés dans certaines commandesGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@891 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau lexeme METAIDENT pour les $idGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@890 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout diverses entrées pour les noms qualifiésGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@889 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout implicits_of_global + accès par noms longsGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@888 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tables séparées pour chaque type de globalGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@887 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement des hacks pour les noms longs par un appel à ↵Gravatar herbelin2000-11-20
| | | | | | Declare.global_qualified_reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@886 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de global_reference dans rawconstrGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@885 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des noms qualifiés dans certaines commandesGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@884 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte noms longsGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@883 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tables séparées pour chaque type de global; calcul de la Nametab de la ↵Gravatar herbelin2000-11-20
| | | | | | 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
* Acceptation des noms qualifiés; utilisation de global_reference dans ↵Gravatar herbelin2000-11-20
| | | | | | 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
* Nouvelle entrée qualidarg pour noms qualifiés; nouveau lexeme METAIDENT ↵Gravatar herbelin2000-11-20
| | | | | | pour les $id git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@880 85f007b7-540e-0410-9357-904b9bb8a0f7
* Acceptation des noms qualifiés; nouveau lexeme METAIDENT pour les $idGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@879 85f007b7-540e-0410-9357-904b9bb8a0f7
* "Distinction entre . suivi d'un blanc et . suivi d'un ident (pour les noms ↵Gravatar herbelin2000-11-20
| | | | | | 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
* MAJGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de global_reference dans patternGravatar herbelin2000-11-20
| | | | 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.39.1) at 2024-07-08 02:38:15 +0000