fixup: Compatibility with 9.1

Author: yannl35133

template-rocq/src/ast_quoter.ml

@@ -103,6 +103,7 @@ struct
   let quote_qvar q =
     match Sorts.QVar.repr q with
     | Sorts.QVar.Var i -> BasicAst.QVar.var (quote_int i)
+    | Sorts.QVar.Global _ -> CErrors.anomaly Pp.(str "Global sort variables cannot be quoted yet.")
     | Sorts.QVar.Unif _ -> CErrors.anomaly (Pp.str "Cannot quote a non-instantiated quality variable")
 
   let quote_quality q =
@@ -216,7 +217,7 @@ struct
   let quote_abstract_univ_context uctx : quoted_abstract_univ_context =
     let {UVars.quals = qnames; UVars.univs = unames} = UVars.AbstractContext.names uctx in
     let qnames = CArray.map_to_list quote_name qnames in
-    let levels = CArray.map_to_list quote_name unames in
+    let unames = CArray.map_to_list quote_name unames in
     let constraints = UVars.UContext.constraints (UVars.AbstractContext.repr uctx) in
     (Universes0.mk_bound_names qnames unames, quote_univ_constraints constraints)
 

template-rocq/src/constr_quoter.ml

@@ -237,7 +237,8 @@ struct
   let quote_qvar q =
     match Sorts.QVar.repr q with
     | Sorts.QVar.Var i -> constr_mkApp (qvVar, [| quote_int i |])
-    | Sorts.QVar.Unif _ -> CErrors.anomaly (str "Non-instanciated quality variables cannot be quoted.")
+    | Sorts.QVar.Global _ -> CErrors.anomaly (str "Global sort variables cannot be quoted yet.")
+    | Sorts.QVar.Unif _ -> CErrors.anomaly (str "Non-instantiated quality variables cannot be quoted.")
 
   let quote_quality q =
     let open Sorts.Quality in

template-rocq/theories/AstUtils.v

@@ -759,14 +759,14 @@ Section Lookups.
     | _ => None
     end.
 
-  Definition lookup_ind_type ind i (u : list Level.t) :=
+  Definition lookup_ind_type ind i u :=
     match lookup_ind_decl ind i with
     |None => None
     |Some res =>
        Some (subst_instance u (snd res).(ind_type))
     end.
 
-  Definition lookup_ind_type_cstrs ind i (u : list Level.t) :=
+  Definition lookup_ind_type_cstrs ind i u :=
     match lookup_ind_decl ind i with
     |None => None
     |Some res =>