aboutsummaryrefslogtreecommitdiff
path: root/interp/coqlib.ml
AgeCommit message (Collapse)Author
2003-11-04Extension de zarithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4790 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ↵herbelin
dans la biblio standard git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4753 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Optimisation de gen_constant_in_modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4689 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14identityT = identityherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4633 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10identity est equivalent sur Type (sauf sans argument)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4592 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Un peu plus de souplesse dans la globalisation des noms utilises par les ↵herbelin
tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4478 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12open superfluherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4356 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Déplacement traducteur de nom dans Constrextern pour accès aux noms longsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4126 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Restructuration des procédures de filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4032 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Mise en place d'un traducteur de noms v7->v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3823 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3815 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29eq fusionne avec eqT et devient par défaut sur Type,herbelin
idem pour ex et exT, ex2 et exT2, all et allT git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3812 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 08:30:10 +0000