Fix test-suite due to changes in 8.18

Author: mattam82

test-suite/tmFix.v

@@ -72,17 +72,17 @@ Module Unquote.
   (* idk why this is needed... *)
   #[local] Hint Extern 1 (Monad _) => refine TemplateMonad_Monad : typeclass_instances.
   Definition tmQuoteSort@{U t u} : TemplateMonad@{t u} sort
-    := p <- @tmQuote Prop (Type@{U} -> True);;
+    := bind@{t u} (@tmQuote@{t u} Prop (Type@{U} -> True)) (fun p =>
       match p with
-      | tProd _ (tSort s) _ => ret s
+      | tProd _ (tSort s) _ => ret@{t u} s
       | _ => tmFail "Anomaly: tmQuote (Type -> True) should be (tProd _ (tSort _) _)!"%bs
-      end.
+      end).
   Definition tmQuoteUniverse@{U t u} : TemplateMonad@{t u} Universe.t
-    := s <- @tmQuoteSort@{U t u};;
+    := bind@{t u} (@tmQuoteSort@{U t u}) (fun s =>
       match s with
       | sType u => ret u
       | _ => tmFail "Sort does not carry a universe (is not Type)"%bs
-      end.
+      end).
   Definition tmQuoteLevel@{U t u} : TemplateMonad@{t u} Level.t
     := bind@{t u} tmQuoteUniverse@{U t u}
        (fun u =>