Use a more systematic mangling of universe names

This should hopefully both speed things up and potentially avoid universe inconsistencies. <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 27m56.55s | 1728408 ko | Total Time / Peak Mem | 35m28.28s | 1976000 ko || -7m31.72s || -247592 ko | -21.22% | -12.52% ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 3m44.84s | 1368456 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.vo | 4m28.56s | 1347576 ko || -0m43.71s || 20880 ko | -16.27% | +1.54% 1m38.93s | 1412680 ko | ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.vo | 2m13.30s | 1674924 ko || -0m34.37s || -262244 ko | -25.78% | -15.65% 0m29.41s | 1116164 ko | ToTemplate/QuotationOf/Common/EnvironmentTyping/Sig.vo | 0m56.50s | 1261512 ko || -0m27.08s || -145348 ko | -47.94% | -11.52% 3m18.00s | 1722424 ko | ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.vo | 3m42.94s | 1976000 ko || -0m24.93s || -253576 ko | -11.18% | -12.83% 0m52.40s | 878548 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.vo | 1m16.86s | 1041496 ko || -0m24.46s || -162948 ko | -31.82% | -15.64% 0m50.59s | 872104 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.vo | 1m14.63s | 1028104 ko || -0m24.03s || -156000 ko | -32.21% | -15.17% 1m00.31s | 1284464 ko | ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.vo | 1m23.83s | 1355772 ko || -0m23.51s || -71308 ko | -28.05% | -5.25% 0m48.68s | 857164 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.vo | 1m10.88s | 997404 ko || -0m22.19s || -140240 ko | -31.32% | -14.06% 0m47.98s | 864128 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.vo | 1m10.28s | 1009492 ko || -0m22.30s || -145364 ko | -31.73% | -14.39% 1m29.10s | 1275632 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.vo | 1m49.82s | 1297876 ko || -0m20.71s || -22244 ko | -18.86% | -1.71% 1m21.35s | 1275952 ko | ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.vo | 1m40.69s | 1293716 ko || -0m19.34s || -17764 ko | -19.20% | -1.37% 1m22.80s | 1276260 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.vo | 1m41.41s | 1301716 ko || -0m18.60s || -25456 ko | -18.35% | -1.95% 0m29.22s | 909244 ko | ToTemplate/QuotationOf/Common/Environment/Sig.vo | 0m46.57s | 1017928 ko || -0m17.35s || -108684 ko | -37.25% | -10.67% 0m52.42s | 1086680 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.vo | 1m07.19s | 1140600 ko || -0m14.76s || -53920 ko | -21.98% | -4.72% 0m45.23s | 1003852 ko | ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.vo | 0m58.27s | 1188136 ko || -0m13.04s || -184284 ko | -22.37% | -15.51% 0m10.48s | 749904 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.vo | 0m21.82s | 876040 ko || -0m11.33s || -126136 ko | -51.97% | -14.39% 0m10.69s | 741580 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.vo | 0m20.21s | 840224 ko || -0m09.52s || -98644 ko | -47.10% | -11.74% 0m21.51s | 803672 ko | ToTemplate/QuotationOf/Template/Ast/Env/Instances.vo | 0m29.88s | 846932 ko || -0m08.36s || -43260 ko | -28.01% | -5.10% 0m11.25s | 747288 ko | ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.vo | 0m19.67s | 833044 ko || -0m08.42s || -85756 ko | -42.80% | -10.29% 0m10.08s | 773444 ko | ToTemplate/QuotationOf/Template/Typing/TemplateGlobalMaps/Instances.vo | 0m18.07s | 819904 ko || -0m07.99s || -46460 ko | -44.21% | -5.66% 0m38.44s | 931460 ko | ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.vo | 0m45.20s | 1013316 ko || -0m06.76s || -81856 ko | -14.95% | -8.07% 0m08.30s | 727596 ko | ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.vo | 0m14.55s | 787268 ko || -0m06.25s || -59672 ko | -42.95% | -7.57% 0m08.17s | 796076 ko | ToTemplate/QuotationOf/Template/Typing/TemplateEnvTyping/Instances.vo | 0m13.50s | 826120 ko || -0m05.33s || -30044 ko | -39.48% | -3.63% 0m07.35s | 717660 ko | ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.vo | 0m12.66s | 785100 ko || -0m05.31s || -67440 ko | -41.94% | -8.58% 0m06.84s | 697892 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.vo | 0m11.49s | 723484 ko || -0m04.65s || -25592 ko | -40.46% | -3.53% 1m38.20s | 1728408 ko | ToTemplate/Coq/MSets.vo | 1m41.31s | 1939012 ko || -0m03.10s || -210604 ko | -3.06% | -10.86% 0m04.03s | 703936 ko | ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.vo | 0m07.25s | 726368 ko || -0m03.21s || -22432 ko | -44.41% | -3.08% 0m04.04s | 698904 ko | ToTemplate/QuotationOf/Coq/FSets/FMapInterface/Sig.vo | 0m06.85s | 724692 ko || -0m02.80s || -25788 ko | -41.02% | -3.55% 0m03.94s | 747208 ko | ToTemplate/QuotationOf/Template/Ast/TemplateLookup/Instances.vo | 0m06.55s | 759832 ko || -0m02.60s || -12624 ko | -39.84% | -1.66% 0m02.47s | 698728 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.vo | 0m04.68s | 708696 ko || -0m02.20s || -9968 ko | -47.22% | -1.40% 0m03.70s | 769896 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversion/Instances.vo | 0m04.88s | 771648 ko || -0m01.17s || -1752 ko | -24.18% | -0.22% 0m02.64s | 921532 ko | ToTemplate/QuotationOf/Template/Ast/EnvHelper/Instances.vo | 0m04.02s | 926344 ko || -0m01.37s || -4812 ko | -34.32% | -0.51% 0m02.63s | 700724 ko | ToTemplate/QuotationOf/Common/Universes/Level/Instances.vo | 0m04.09s | 700076 ko || -0m01.46s || 648 ko | -35.69% | +0.09% 0m02.38s | 758748 ko | ToTemplate/QuotationOf/Template/Typing/TemplateDeclarationTyping/Instances.vo | 0m04.17s | 759436 ko || -0m01.79s || -688 ko | -42.92% | -0.09% 0m02.04s | 701080 ko | ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.vo | 0m03.37s | 698344 ko || -0m01.33s || 2736 ko | -39.46% | +0.39% 0m01.94s | 701404 ko | ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.vo | 0m03.28s | 697440 ko || -0m01.33s || 3964 ko | -40.85% | +0.56% 0m01.69s | 700096 ko | ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.vo | 0m02.81s | 705736 ko || -0m01.12s || -5640 ko | -39.85% | -0.79% 1m01.47s | 1389880 ko | ToTemplate/Coq/FSets.vo | 1m01.73s | 1402124 ko || -0m00.25s || -12244 ko | -0.42% | -0.87% 0m26.12s | 1284060 ko | ToTemplate/Common/EnvironmentTyping.vo | 0m26.92s | 1338856 ko || -0m00.80s || -54796 ko | -2.97% | -4.09% 0m20.82s | 1095908 ko | ToTemplate/Template/Typing.vo | 0m20.40s | 1099736 ko || +0m00.42s || -3828 ko | +2.05% | -0.34% 0m18.82s | 908440 ko | ToTemplate/Common/Universes.vo | 0m18.48s | 916460 ko || +0m00.33s || -8020 ko | +1.83% | -0.87% 0m15.43s | 868820 ko | ToTemplate/Common/Kernames.vo | 0m14.86s | 872484 ko || +0m00.57s || -3664 ko | +3.83% | -0.41% 0m06.58s | 998568 ko | ToTemplate/Template/TermEquality.vo | 0m07.01s | 1005820 ko || -0m00.42s || -7252 ko | -6.13% | -0.72% 0m06.30s | 995716 ko | ToTemplate/Template/WfAst.vo | 0m06.50s | 1002992 ko || -0m00.20s || -7276 ko | -3.07% | -0.72% 0m05.88s | 935032 ko | ToTemplate/Common/Environment.vo | 0m06.47s | 950944 ko || -0m00.58s || -15912 ko | -9.11% | -1.67% 0m03.62s | 699480 ko | ToTemplate/QuotationOf/Coq/Structures/Equalities/Sig.vo | 0m03.88s | 702452 ko || -0m00.25s || -2972 ko | -6.70% | -0.42% 0m03.10s | 711792 ko | ToTemplate/Coq/Init.vo | 0m02.70s | 705556 ko || +0m00.39s || 6236 ko | +14.81% | +0.88% 0m02.90s | 990412 ko | ToTemplate/Template/Ast.vo | 0m03.14s | 999436 ko || -0m00.24s || -9024 ko | -7.64% | -0.90% 0m02.35s | 696844 ko | ToTemplate/Init.vo | 0m02.30s | 699476 ko || +0m00.05s || -2632 ko | +2.17% | -0.37% 0m02.35s | 699696 ko | ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.vo | 0m03.12s | 700204 ko || -0m00.77s || -508 ko | -24.67% | -0.07% 0m02.01s | 1003068 ko | ToTemplate/All.vo | 0m01.89s | 1010272 ko || +0m00.11s || -7204 ko | +6.34% | -0.71% 0m01.96s | 696624 ko | ToTemplate/Utils/All_Forall.vo | 0m01.91s | 696852 ko || +0m00.05s || -228 ko | +2.61% | -0.03% 0m01.89s | 757188 ko | ToTemplate/QuotationOf/Template/Typing/TemplateTyping/Instances.vo | 0m02.02s | 756856 ko || -0m00.13s || 332 ko | -6.43% | +0.04% 0m01.84s | 705696 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTerm/Instances.vo | 0m02.58s | 710328 ko || -0m00.74s || -4632 ko | -28.68% | -0.65% 0m01.76s | 697100 ko | CommonUtils.vo | 0m01.36s | 697944 ko || +0m00.39s || -844 ko | +29.41% | -0.12% 0m01.62s | 700016 ko | ToTemplate/Coq/Numbers.vo | 0m01.16s | 700136 ko || +0m00.46s || -120 ko | +39.65% | -0.01% 0m01.59s | 712640 ko | ToTemplate/QuotationOf/Template/ReflectAst/EnvDecide/Instances.vo | 0m01.97s | 712756 ko || -0m00.37s || -116 ko | -19.28% | -0.01% 0m01.54s | 694776 ko | ToTemplate/Utils/MCOption.vo | 0m01.99s | 696804 ko || -0m00.44s || -2028 ko | -22.61% | -0.29% 0m01.52s | 870516 ko | ToTemplate/Common/BasicAst.vo | 0m01.60s | 877576 ko || -0m00.08s || -7060 ko | -5.00% | -0.80% 0m01.51s | 694220 ko | ToTemplate/Utils/MCReflect.vo | 0m01.51s | 694328 ko || +0m00.00s || -108 ko | +0.00% | -0.01% 0m01.50s | 960280 ko | ToTemplate/QuotationOf/Template/Ast/Instances.vo | 0m01.55s | 968092 ko || -0m00.05s || -7812 ko | -3.22% | -0.80% 0m01.49s | 693456 ko | ToTemplate/Utils/MCProd.vo | 0m01.50s | 694308 ko || -0m00.01s || -852 ko | -0.66% | -0.12% 0m01.46s | 985456 ko | ToTemplate/Template/AstUtils.vo | 0m01.64s | 995224 ko || -0m00.17s || -9768 ko | -10.97% | -0.98% 0m01.45s | 704060 ko | ToTemplate/Coq/Floats.vo | 0m01.01s | 703292 ko || +0m00.43s || 768 ko | +43.56% | +0.10% 0m01.36s | 697084 ko | ToTemplate/Coq/Lists.vo | 0m01.36s | 698156 ko || +0m00.00s || -1072 ko | +0.00% | -0.15% 0m01.35s | 700116 ko | ToTemplate/Utils/utils.vo | 0m01.26s | 700996 ko || +0m00.09s || -880 ko | +7.14% | -0.12% 0m01.34s | 693840 ko | ToTemplate/Coq/ssr.vo | 0m01.14s | 694884 ko || +0m00.20s || -1044 ko | +17.54% | -0.15% 0m01.33s | 694508 ko | ToTemplate/Utils/MCUtils.vo | 0m01.16s | 694536 ko || +0m00.17s || -28 ko | +14.65% | -0.00% 0m01.32s | 710140 ko | ToTemplate/QuotationOf/Template/ReflectAst/TemplateTermDecide/Instances.vo | 0m01.40s | 711564 ko || -0m00.07s || -1424 ko | -5.71% | -0.20% 0m01.29s | 754500 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversionPar/Instances.vo | 0m01.57s | 755212 ko || -0m00.28s || -712 ko | -17.83% | -0.09% 0m01.27s | 756972 ko | ToTemplate/QuotationOf/Template/Typing/Instances.vo | 0m01.17s | 756196 ko || +0m00.10s || 776 ko | +8.54% | +0.10% 0m01.24s | 694592 ko | ToTemplate/Coq/Bool.vo | 0m01.43s | 695096 ko || -0m00.18s || -504 ko | -13.28% | -0.07% 0m01.20s | 746972 ko | ToTemplate/QuotationOf/Common/Universes/Instances.vo | 0m01.06s | 754076 ko || +0m00.13s || -7104 ko | +13.20% | -0.94% 0m01.20s | 693144 ko | ToTemplate/Utils/bytestring.vo | 0m01.53s | 698048 ko || -0m00.33s || -4904 ko | -21.56% | -0.70% 0m01.19s | 765652 ko | ToTemplate/QuotationOf/Common/Kernames/Instances.vo | 0m01.09s | 771052 ko || +0m00.09s || -5400 ko | +9.17% | -0.70% 0m01.18s | 704780 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTermUtils/Instances.vo | 0m01.70s | 707492 ko || -0m00.52s || -2712 ko | -30.58% | -0.38% 0m01.11s | 692748 ko | ToTemplate/Common/Primitive.vo | 0m01.25s | 693068 ko || -0m00.13s || -320 ko | -11.19% | -0.04% 0m01.09s | 695940 ko | ToTemplate/Coq/Strings.vo | 0m01.01s | 694968 ko || +0m00.08s || 972 ko | +7.92% | +0.13% 0m01.08s | 694044 ko | ToTemplate/Utils/ReflectEq.vo | 0m01.16s | 693864 ko || -0m00.07s || 180 ko | -6.89% | +0.02% 0m01.03s | 701348 ko | ToTemplate/QuotationOf/Template/ReflectAst/Instances.vo | 0m01.07s | 700708 ko || -0m00.04s || 640 ko | -3.73% | +0.09% 0m01.02s | 698120 ko | ToTemplate/Utils/MCList.vo | 0m01.29s | 693604 ko || -0m00.27s || 4516 ko | -20.93% | +0.65% 0m01.01s | 693148 ko | ToTemplate/Common/config.vo | 0m01.23s | 694780 ko || -0m00.21s || -1632 ko | -17.88% | -0.23% 0m01.01s | 695988 ko | ToTemplate/Utils/MCArith.vo | 0m01.19s | 693928 ko || -0m00.17s || 2060 ko | -15.12% | +0.29% 0m00.07s | 63164 ko | ToTemplate/Utils/MCEquality.vo | 0m00.04s | 63060 ko || +0m00.03s || 104 ko | +75.00% | +0.16% 0m00.07s | 63300 ko | ToTemplate/Utils/MCPred.vo | 0m00.03s | 63976 ko || +0m00.04s || -676 ko | +133.33% | -1.05% 0m00.07s | 64460 ko | ToTemplate/Utils/MCString.vo | 0m00.05s | 64348 ko || +0m00.02s || 112 ko | +40.00% | +0.17% 0m00.07s | 64916 ko | ToTemplate/Utils/monad_utils.vo | 0m00.06s | 63088 ko || +0m00.01s || 1828 ko | +16.66% | +2.89% 0m00.06s | 63864 ko | ToTemplate/Utils/LibHypsNaming.vo | 0m00.04s | 64692 ko || +0m00.01s || -828 ko | +49.99% | -1.27% 0m00.06s | 64556 ko | ToTemplate/Utils/MCCompare.vo | 0m00.06s | 64992 ko || +0m00.00s || -436 ko | +0.00% | -0.67% 0m00.06s | 62916 ko | ToTemplate/Utils/MCPrelude.vo | 0m00.07s | 63064 ko || -0m00.01s || -148 ko | -14.28% | -0.23% 0m00.06s | 64596 ko | ToTemplate/Utils/MCRelations.vo | 0m00.07s | 64120 ko || -0m00.01s || 476 ko | -14.28% | +0.74% 0m00.06s | 66120 ko | ToTemplate/Utils/wGraph.vo | 0m00.06s | 64668 ko || +0m00.00s || 1452 ko | +0.00% | +2.24% 0m00.05s | 67780 ko | ToTemplate/Common/Reflect.vo | 0m00.07s | 63112 ko || -0m00.02s || 4668 ko | -28.57% | +7.39% 0m00.05s | 64504 ko | ToTemplate/Template/LiftSubst.vo | 0m00.05s | 63644 ko || +0m00.00s || 860 ko | +0.00% | +1.35% 0m00.05s | 64312 ko | ToTemplate/Utils/ByteCompare.vo | 0m00.05s | 63780 ko || +0m00.00s || 532 ko | +0.00% | +0.83% 0m00.05s | 63592 ko | ToTemplate/Utils/ByteCompareSpec.vo | 0m00.04s | 64228 ko || +0m00.01s || -636 ko | +25.00% | -0.99% 0m00.04s | 63060 ko | ToTemplate/Common/Transform.vo | 0m00.05s | 64720 ko || -0m00.01s || -1660 ko | -20.00% | -2.56% 0m00.04s | 63428 ko | ToTemplate/Template/ReflectAst.vo | 0m00.05s | 64352 ko || -0m00.01s || -924 ko | -20.00% | -1.43% 0m00.04s | 63860 ko | ToTemplate/Utils/MCSquash.vo | 0m00.06s | 63524 ko || -0m00.01s || 336 ko | -33.33% | +0.52% 0m00.03s | 64740 ko | ToTemplate/Template/Induction.vo | 0m00.05s | 64888 ko || -0m00.02s || -148 ko | -40.00% | -0.22% 0m00.03s | 64172 ko | ToTemplate/Template/UnivSubst.vo | 0m00.02s | 63464 ko || +0m00.00s || 708 ko | +49.99% | +1.11% 0m00.03s | 63548 ko | ToTemplate/Utils/ByteCompare_opt.vo | 0m00.05s | 64136 ko || -0m00.02s || -588 ko | -40.00% | -0.91% ``` </p> </details>
MetaCoq · Apr 7, 2023 · 8bd85e5 · 8bd85e5
1 parent bd06ca1
commit 8bd85e5
Show file tree

Hide file tree

Showing 2 changed files with 86 additions and 135 deletions.
diff --git a/quotation/theories/CommonUtils.v b/quotation/theories/CommonUtils.v
@@ -223,71 +223,6 @@ Module WithTemplate.
          end.
   End with_monad.
 
-  #[local] Definition CacheT T : Type := term * list term * UniverseMap.t term -> T * (term * list term * UniverseMap.t term).
-  #[local] Instance CacheT_Monad : Monad CacheT
-    := {| ret A v := fun st => (v, st)
-       ; bind A B v f := fun st => let '(v, st) := v st in f v st |}.
-  #[local] Definition init_cache_and_run (lProp_t lSProp_t lSet_t : term) (default_univ : term) (available_univs : list term) {T} : CacheT T -> T
-    := fun f
-       => fst
-            (f (default_univ,
-                 available_univs,
-                 UniverseMap.add
-                   Universe.lProp lProp_t
-                   (UniverseMap.add
-                      Universe.lSProp lSProp_t
-                      (UniverseMap.add
-                         (Universe.of_levels (inr Level.lzero)) lSet_t
-                         (UniverseMap.empty _))))).
-  #[local] Definition lookupU (u : Universe.t) : CacheT term
-    := fun '((default_univ, fresh_univs, map) as st)
-       => match UniverseMap.find u map, fresh_univs with
-          | Some t, _ => (t, st)
-          | None, nil => (default_univ, st)
-          | None, t :: fresh_univs
-            => (t, (default_univ, fresh_univs, UniverseMap.add u t map))
-          end.
-
-  #[local]
-    Definition tmRelaxSortsCached (in_domain : bool) (do_replace_U : Universe.t -> bool) (lProp_t lSProp_t lSet_t : term) (default_univ : term) (available_univs : list term) (t : term) : term
-    := init_cache_and_run
-         lProp_t lSProp_t lSet_t default_univ available_univs
-         (tmRelaxSortsM
-            in_domain
-            (fun u => if do_replace_U u
-                      then lookupU u
-                      else ret (tSort u))
-            t).
-
-  Polymorphic Inductive list_of_types@{u} : Type@{u+1} := nil | cons (x : Type@{u}) (xs : list_of_types).
-  Declare Scope list_of_types_scope.
-  Delimit Scope list_of_types_scope with list_of_types.
-  Bind Scope list_of_types_scope with list_of_types.
-
-  Infix "::" := cons : list_of_types_scope.
-  Notation "[ ]" := nil : list_of_types_scope.
-  Notation "[ x ]" := (cons x nil) : list_of_types_scope.
-  Notation "[ x ; y ; .. ; z ]" :=  (cons x (cons y .. (cons z nil) ..))  : list_of_types_scope.
-
-  Polymorphic Definition types_monad_map@{l b a t u} {T} {M : Monad@{t u} T} {B : Type@{b}} (f : Type@{a} -> T B)
-    := fix types_monad_map (l : list_of_types@{l}) : T (list B)
-      := match l with
-         | []%list_of_types => ret []%list
-         | (x :: xs)%list_of_types
-           => fx <- f x;;
-              fxs <- types_monad_map xs;;
-              ret (fx :: fxs)%list
-         end.
-
-  #[local] Polymorphic Definition tmRelaxSortsQuote@{uP uSP uS uD uL t u _high} (in_domain : bool) (do_replace_U : Universe.t -> bool) (available_univs : list_of_types@{uL}) (t : term) : TemplateMonad@{t u} term
-    := lProp_t <- @tmQuote Type@{_high} Type@{uP};;
-       lSProp_t <- @tmQuote Type@{_high} Type@{uSP};;
-       lSet_t <- @tmQuote Type@{_high} Type@{uS};;
-       default_univ <- @tmQuote Type@{_high} Type@{uD};;
-       available_univs <- types_monad_map@{uL _high _ _ _} tmQuote available_univs;;
-       ret (tmRelaxSortsCached in_domain do_replace_U lProp_t lSProp_t lSet_t default_univ available_univs t).
-
-
   #[local] Definition is_set (s : Universe.t) : bool
     := match option_map Level.is_set (Universe.get_is_level s) with
        | Some true => true
@@ -306,77 +241,91 @@ Module WithTemplate.
        | _ => false
        end.
 
-  Polymorphic Definition tmRetypeMagicRelaxSetInCodomain@{U a b t u _high} {A : Type@{a}} (B : Type@{b}) (x : A) : TemplateMonad@{t u} B
+  Definition tmRelaxSet (in_domain : bool) (prefix : string) (t : term) : term
+    := tmRelaxSortsM
+         (M:=fun T => T) in_domain
+         (fun u => tSort (if is_set u then Universe.of_levels (inr (Level.Level (prefix ++ "._Set.0")%bs)) else u))
+         t.
+
+  Module Import PrefixUniverse.
+    Module Level.
+      Definition prefix_with (prefix : string) (l : Level.t) : Level.t
+        := match l with
+           | Level.lzero | Level.Var _ => l
+           | Level.Level u => Level.Level (prefix ++ "." ++ u)%bs
+           end.
+    End Level.
+
+    Module LevelExprSet.
+      Module Raw.
+        Definition prefix_with (prefix : string) (l : LevelExprSet.Raw.t) : LevelExprSet.Raw.t
+          := List.map (fun '(l, n) => (Level.prefix_with prefix l, n)) l.
+      End Raw.
+      Lemma prefix_with_Ok {prefix : string} {l : LevelExprSet.Raw.t} (pf : LevelExprSet.Raw.Ok l) : LevelExprSet.Raw.Ok (Raw.prefix_with prefix l).
+      Proof.
+        hnf in *; cbv [Raw.prefix_with] in *; cbn in *.
+        induction l as [|[l n] ls IH]; cbn in *; [ reflexivity | ].
+        apply Bool.andb_true_iff in pf; destruct pf as [pf1 pf2].
+        rewrite IH, Bool.andb_true_r by assumption.
+        clear IH pf2.
+        destruct ls as [|[l' n'] ls]; cbn in *; [ reflexivity | ].
+        destruct l, l'; cbn in *; try assumption.
+        induction prefix as [|?? IH];
+          cbn in *; try assumption.
+        rewrite ByteCompareSpec.compare_eq_refl; assumption.
+      Qed.
+      Definition prefix_with (prefix : string) (l : LevelExprSet.t) : LevelExprSet.t
+        := @LevelExprSet.Mkt (Raw.prefix_with prefix (@LevelExprSet.this l)) (prefix_with_Ok (@LevelExprSet.is_ok l)).
+      Lemma is_empty_prefix_with {prefix} {l} : LevelExprSet.is_empty (prefix_with prefix l) = LevelExprSet.is_empty l.
+      Proof.
+        destruct l as [l pf]; cbn.
+        cbv [LevelExprSet.is_empty prefix_with LevelExprSet.Raw.is_empty]; cbn.
+        destruct l; cbn; reflexivity.
+      Qed.
+    End LevelExprSet.
+
+    Module nonEmptyLevelExprSet.
+      Definition prefix_with (prefix : string) (l : nonEmptyLevelExprSet) : nonEmptyLevelExprSet
+        := {| t_set := LevelExprSet.prefix_with prefix l.(t_set)
+           ; t_ne := eq_trans LevelExprSet.is_empty_prefix_with l.(t_ne) |}.
+    End nonEmptyLevelExprSet.
+
+    Module LevelAlgExpr := nonEmptyLevelExprSet.
+
+    Module Universe.
+      Definition prefix_with (prefix : string) (u : Universe.t) : Universe.t
+        := match u with
+           | Universe.lProp | Universe.lSProp => u
+           | Universe.lType u => Universe.lType (LevelAlgExpr.prefix_with prefix u)
+           end.
+    End Universe.
+  End PrefixUniverse.
+
+  Definition tmRelaxOnlyType (in_domain : bool) (prefix : string) (t : term) : term
+    := tmRelaxSortsM
+         (M:=fun T => T) in_domain
+         (fun u => tSort (PrefixUniverse.Universe.prefix_with prefix u))
+         t.
+
+  Polymorphic Definition tmRetypeMagicRelaxSetInCodomain@{a b t u} (prefix : string) {A : Type@{a}} (B : Type@{b}) (x : A) : TemplateMonad@{t u} B
     := qx <- tmQuote x;;
-       qx <- tmRelaxSortsQuote@{U U U U _high t u _high} false is_set [] qx;;
+       let qx := tmRelaxSet false prefix qx in
        tmUnquoteTyped B qx.
-  Polymorphic Definition tmRetypeRelaxSetInCodomain@{U a t u _high} {A : Type@{a}} (x : A) : TemplateMonad@{t u} A
-    := tmRetypeMagicRelaxSetInCodomain@{U a a t u _high} A x.
+  Polymorphic Definition tmRetypeRelaxSetInCodomain@{a t u} (prefix : string) {A : Type@{a}} (x : A) : TemplateMonad@{t u} A
+    := tmRetypeMagicRelaxSetInCodomain@{a a t u} prefix A x.
 
-  Local Notation many_Types_2 tail := (Type :: Type :: Type :: Type :: tail)%list_of_types (only parsing).
-  Local Notation many_Types_3 tail := (many_Types_2 (many_Types_2 tail)) (only parsing).
-  Local Notation many_Types_4 tail := (many_Types_3 (many_Types_3 tail)) (only parsing).
-  Local Notation many_Types_5 tail := (many_Types_4 (many_Types_4 tail)) (only parsing).
-  Local Notation many_Types := (many_Types_5 nil) (only parsing).
-
-  Polymorphic Definition tmRetypeMagicRelaxOnlyType0@{U a b t u _high} {A : Type@{a}} (B : Type@{b}) (x : A) : TemplateMonad@{t u} B
+  Polymorphic Definition tmRetypeMagicRelaxOnlyType@{a b t u} (prefix : string) {A : Type@{a}} (B : Type@{b}) (x : A) : TemplateMonad@{t u} B
     := qx <- tmQuote x;;
-       qx <- tmRelaxSortsQuote@{U U U U _high t u _high} true is_only_type [] qx;;
+       let qx := tmRelaxOnlyType true prefix qx in
        tmUnquoteTyped B qx.
-  Polymorphic Definition tmRetypeRelaxOnlyType0@{U a t u _high} {A : Type@{a}} (x : A) : TemplateMonad@{t u} A
-    := tmRetypeMagicRelaxOnlyType0@{U a a t u _high} A x.
-
-  Polymorphic Definition tmRetypeMagicRelaxOnlyType {A : Type} (B : Type) (x : A) : TemplateMonad B
-    := qx <- tmQuote x;;
-       qx <- tmRelaxSortsQuote true is_only_type many_Types qx;;
-       tmUnquoteTyped B qx.
-  Polymorphic Definition tmRetypeRelaxOnlyType {A} (x : A) : TemplateMonad A
-    := tmRetypeMagicRelaxOnlyType A x.
+  Polymorphic Definition tmRetypeRelaxOnlyType@{a t u} (prefix : string) {A : Type@{a}} (x : A) : TemplateMonad@{t u} A
+    := tmRetypeMagicRelaxOnlyType@{a a t u} prefix A x.
 
   (* Hack around https://github.com/MetaCoq/metacoq/issues/853 *)
-  Polymorphic Definition tmRetypeAroundMetaCoqBug853_0 (t : typed_term) : TemplateMonad typed_term
-    := let '{| my_projT1 := ty ; my_projT2 := v |} := t in
-       ty <- tmRetypeRelaxOnlyType0 ty;;
-       v <- tmRetypeMagicRelaxOnlyType0 ty v;;
-       ret {| my_projT1 := ty ; my_projT2 := v |}.
-
-  Polymorphic Definition tmRetypeAroundMetaCoqBug853_gen (t : typed_term) : TemplateMonad typed_term
+  Definition tmRetypeAroundMetaCoqBug853 (prefix : string) (t : typed_term) : TemplateMonad typed_term
     := let '{| my_projT1 := ty ; my_projT2 := v |} := t in
-       ty <- tmRetypeRelaxOnlyType ty;;
-       v <- tmRetypeMagicRelaxOnlyType ty v;;
+       ty <- tmRetypeRelaxOnlyType prefix ty;;
+       v <- tmRetypeMagicRelaxOnlyType prefix ty v;;
        ret {| my_projT1 := ty ; my_projT2 := v |}.
-
-  (* Hack around https://github.com/MetaCoq/metacoq/pull/876#issuecomment-1487743822 *)
-  Monomorphic Variant exn : Set := GenericError.
-
-  Polymorphic Variant option_try@{u} (A : Type@{u}) : Type@{max(Set, u)} := my_Value (val : A) | my_Error (err : exn).
-
-  Arguments my_Value {A} val.
-  Arguments my_Error {A} _.
-  Polymorphic Class tmCheckSuccessHelper@{t u} {A : Type@{t}} (run : TemplateMonad@{t u} A) := tmCheckSuccess_ret : unit.
-  #[global] Hint Extern 0 (tmCheckSuccessHelper ?run) => run_template_program run (fun v => exact tt) : typeclass_instances.
-  Polymorphic Definition tmCheckSuccess@{t u} {A : Type@{t}} (run : TemplateMonad@{t u} A) : TemplateMonad@{t u} bool
-  := tmBind (tmInferInstance None (tmCheckSuccessHelper run))
-            (fun inst => match inst with
-                         | my_Some _ => tmReturn true
-                         | my_None => tmReturn false
-                         end).
-  Polymorphic Definition tmTryWorseButNoAnomaly@{t u} {A : Type@{t}} (run : TemplateMonad@{t u} A) : TemplateMonad@{t u} (option_try@{t} A)
-    := succeeds <- tmCheckSuccess run;;
-       if succeeds:bool
-       then v <- run;; ret (my_Value v)
-       else ret (my_Error GenericError).
-
-  Definition tmRetypeAroundMetaCoqBug853 (t : typed_term) : TemplateMonad typed_term
-    := Eval cbv [List.fold_right] in
-      List.fold_right
-        (fun tmRetype acc
-         => res <- tmTryWorseButNoAnomaly (tmRetype t);;
-            match res with
-            | my_Value v => ret v
-            | my_Error _ => acc
-            end)
-        (tmRetypeAroundMetaCoqBug853_gen t)
-        [tmRetypeAroundMetaCoqBug853_0; tmRetypeAroundMetaCoqBug853_gen].
 End WithTemplate.
 Export WithTemplate (transparentify, tmQuoteToGlobalReference, tmRetypeRelaxSetInCodomain, tmRetypeRelaxOnlyType, tmRetypeMagicRelaxSetInCodomain, tmRetypeMagicRelaxOnlyType, tmObj_magic, tmRetype, tmExtractBaseModPathFromMod, tmRetypeAroundMetaCoqBug853).
diff --git a/quotation/theories/ToTemplate/Init.v b/quotation/theories/ToTemplate/Init.v
@@ -424,7 +424,9 @@ Ltac unfold_quotation_of _ :=
              | change (@quotation_of A (transparentify t)) ]
   end.
 
-Polymorphic Definition tmPrepareMakeQuotationOfConstants@{U t u u' _T _above_u _above_u'} {debug:debug_opt} (work_aronud_coq_bug_17303 : bool) (include_submodule : list ident -> bool) (include_supermodule : list ident -> list ident -> bool) (base : modpath) (cs : list global_reference) : TemplateMonad@{t u} (list (string * typed_term@{u'}))
+(* for universe adjustment with [tmDeclareQuotationOfModule], [tmMakeQuotationOfModule] *)
+#[export] Unset MetaCoq Strict Unquote Universe Mode.
+Polymorphic Definition tmPrepareMakeQuotationOfConstants@{U t u u' _T _above_u _above_u'} {debug:debug_opt} (work_around_coq_bug_17303 : bool) (include_submodule : list ident -> bool) (include_supermodule : list ident -> list ident -> bool) (base : modpath) (cs : list global_reference) : TemplateMonad@{t u} (list (string * typed_term@{u'}))
   := let warn_bad_ctx c ctx :=
        (_ <- tmMsg "tmPrepareMakeQuotationOfModule: cannot handle polymorphism";;
         _ <- tmPrint c;;
@@ -442,7 +444,7 @@ Polymorphic Definition tmPrepareMakeQuotationOfConstants@{U t u u' _T _above_u _
         _ <- tmDebugPrint r;;
         tmReturn []) in
      let make_qname '(mp, name)
-                    (* ideally we'd replace _ with __ so that there can't be any collision, but the utility functions aren't written and we don't need it in practice *)
+       (* ideally we'd replace _ with __ so that there can't be any collision, but the utility functions aren't written and we don't need it in practice *)
        := option_map
             (fun n => "q" ++ n)%bs
             match split_common_prefix base mp with
@@ -488,7 +490,7 @@ Polymorphic Definition tmPrepareMakeQuotationOfConstants@{U t u u' _T _above_u _
                            _ <- tmDebugMsg "tmPrepareMakeQuotationOfConstants: tmUnquote";;
                            '{| my_projT1 := cty ; my_projT2 := cv |} <- tmUnquote c;;
                            _ <- tmDebugMsg "tmPrepareMakeQuotationOfConstants: tmUnquote done";;
-                           tmReturn [(qname, if work_aronud_coq_bug_17303
+                           tmReturn [(qname, if work_around_coq_bug_17303
                                              then {| my_projT1 := term ; my_projT2 := c |}
                                              else {| my_projT1 := @quotation_of cty cv ; my_projT2 := c |})]
                       end
@@ -507,7 +509,7 @@ Polymorphic Definition tmPrepareMakeQuotationOfConstants@{U t u u' _T _above_u _
                            _ <- tmDebugMsg "tmPrepareMakeQuotationOfConstants: tmUnquote";;
                            '{| my_projT1 := cty ; my_projT2 := cv |} <- tmUnquote c;;
                            _ <- tmDebugMsg "tmPrepareMakeQuotationOfConstants: tmUnquote done";;
-                           let tmcty := tmRetypeRelaxSetInCodomain@{U t t u _above_u} cty in
+                           let tmcty := tmRetypeRelaxSetInCodomain@{t t u} qname cty in
                            _ <- tmDebugPrint tmcty;;
                            cty <- tmcty;;
                            let tmcv := tmObj_magic (B:=cty) cv in
@@ -524,19 +526,19 @@ Polymorphic Definition tmPrepareMakeQuotationOfConstants@{U t u u' _T _above_u _
      ret ps.
 
 (* N.B. We need to kludge around COQBUG(https://github.com/coq/coq/issues/17303) in Kernames :-( *)
-Polymorphic Definition tmMakeQuotationOfConstants_gen@{U d t u u' _T _above_u _above_u' _above_gr} {debug:debug_opt} (work_aronud_coq_bug_17303 : bool) (include_submodule : list ident -> bool) (include_supermodule : list ident -> list ident -> bool) (existing_instance : option hint_locality) (base : modpath) (cs : list global_reference) (tmDoWithDefinition : ident -> forall A : Type@{d}, A -> TemplateMonad A) : TemplateMonad unit
+Polymorphic Definition tmMakeQuotationOfConstants_gen@{U d t u u' _T _above_u _above_u' _above_gr} {debug:debug_opt} (work_around_coq_bug_17303 : bool) (include_submodule : list ident -> bool) (include_supermodule : list ident -> list ident -> bool) (existing_instance : option hint_locality) (base : modpath) (cs : list global_reference) (tmDoWithDefinition : ident -> forall A : Type@{d}, A -> TemplateMonad A) : TemplateMonad unit
   := let tmDebugMsg s := (if debug
                           then tmMsg s
                           else tmReturn tt) in
      let tmDebugPrint {T : Type@{_T}} (v : T)
        := (if debug
            then tmPrint v
            else tmReturn tt) in
-     ps <- tmPrepareMakeQuotationOfConstants@{U t u u' _T _above_u _above_u'} work_aronud_coq_bug_17303 include_submodule include_supermodule base cs;;
+     ps <- tmPrepareMakeQuotationOfConstants@{U t u u' _T _above_u _above_u'} work_around_coq_bug_17303 include_submodule include_supermodule base cs;;
      _ <- tmDebugMsg "tmMakeQuotationOfConstants_gen: defining module constants";;
      ps <- monad_map@{_ _ _above_gr _above_u'}
              (fun '(name, tyv)
-              => let tmTyv := tmRetypeAroundMetaCoqBug853 tyv in
+              => let tmTyv := tmRetypeAroundMetaCoqBug853 name tyv in
                  _ <- tmDebugPrint tmTyv;;
                  '{| my_projT1 := ty ; my_projT2 := v |} <- tmTyv;;
                  tmDef_name <- tmEval cbv (@tmDoWithDefinition (name:string));;