aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/TranspModtype.out
AgeCommit message (Collapse)Author
2019-01-09Stop [Print] from saying [is (not) universe polymorphic].Gaëtan Gilbert
[About] still says it. Close #9056.
2018-12-17Stop printing Monomorphic/Polymorphic in Print.Gaëtan Gilbert
You can tell which it is from the `@{}` if you really care, and seeing `Monomorphic List (A:Type)` with no indication that `Monomorphic` is about universes can confuse people.
2018-11-02Remove is_universe_polymorphism from printingGaëtan Gilbert
2015-03-09Do not display the status of monomorphic constants unless in ↵Guillaume Melquiond
universe-polymorphism mode.
2014-08-12Upgrading output tests.Hugo Herbelin
output/Arguments.v output/ArgumentsScope.v output/Arguments_renaming.v output/Cases.v output/Implicit.v output/PrintInfos.v output/TranspModType.v Main changes: monomorphic -> not universe polymorphic, Peano vs Nat
2014-05-08Fixing output test-suite: since universe polymorphism, the Print commandPierre-Marie Pédrot
shows the polymorphism status of the term.
2008-03-25Correction de bugs relatifs a la compostion des substitutionssoubiran
engendrees par les alias de module git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10718 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
kernel: -declaration.ml unification des representations pour les modules et modules types. (type struct_expr_body) -mod_typing.ml le typage des modules est separe de l'evaluation des modules -modops.ml nouvelle fonction qui pour toutes expressions de structure calcule sa forme evaluee.(eval_struct) -safe_typing.ml ajout du support du nouvel operateur Include.(add_include). library: -declaremods.ml nouveaux objets Include et Module-alias et gestion de la resolution de noms pour les alias via la nametab. parsing: -g_vernac.ml4: nouvelles regles pour le support des Includes et pour l'application des signatures fonctorielles. extraction: Adaptation a la nouvelle representation des modules et support de l'operateur with. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10497 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-05Correction de quelques défauts d'affichage (notations sous "as" pourherbelin
filtrage; sauts de line intempestifs dans pretty.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10179 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-22Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7701 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-16Nouvelle syntaxe 'with' des modules non gérée en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6843 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-09Export M + Module M <: SIGcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3494 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:26:09 +0000