Adapt to coq/coq#20178 (UContext.to_context returns qvar set not qual…

…ity set)
MetaCoq · Feb 5, 2025 · 4c031d5 · 4c031d5
1 parent ca7f250
commit 4c031d5
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 10 deletions.
diff --git a/template-coq/src/quoter.ml b/template-coq/src/quoter.ml
@@ -6,10 +6,7 @@ open Pp
 open Tm_util
 open Reification
 
-let inductive_sort mip =
-  match mip.mind_arity with
-  | RegularArity s -> s.mind_sort
-  | TemplateArity ar -> ar.template_level
+let inductive_sort mip = mip.mind_sort
 
 let cast_prop = ref (false)
 
@@ -456,9 +453,7 @@ struct
           (* TODO quote the real squash data instead of approximating with a sort family *)
           let kelim = match oib.Declarations.mind_squashed with
             | None -> Sorts.InType
-            | Some _ -> match oib.mind_arity with
-              | TemplateArity _ -> InType
-              | RegularArity s -> Sorts.family s.mind_sort
+            | Some _ -> Sorts.family oib.mind_sort
           in
           let sf = Q.quote_sort_family kelim in
             (Q.quote_ident oib.mind_typename, indices, indsort, indty, sf,

diff --git a/template-coq/src/tm_util.ml b/template-coq/src/tm_util.ml
@@ -272,9 +272,6 @@ module RetypeMindEntry =
       | Entries.Template_ind_entry uctx -> evm
       | Entries.Polymorphic_ind_entry uctx ->
         let qs, (us, csts) = UVars.UContext.to_context_set uctx in
-        let qs = Sorts.Quality.Set.fold (fun q qs -> match q with
-            | QConstant _ -> assert false
-            | QVar q -> Sorts.QVar.Set.add q qs) qs Sorts.QVar.Set.empty in
         Evd.merge_sort_context_set (UState.UnivFlexible false) evm ((qs,us),csts)
     in
     let evm, mind = infer_mentry_univs env evm mind in