Merge pull request #1145 from SkySkimmer/template-entry-qvar

Adapt to rocq-prover/rocq#20178 (UContext.to_context returns qvar set not quality set)

Author: ppedrot

safechecker-plugin/Makefile

@@ -42,7 +42,7 @@ mrproper:
 	rm -f Makefile.safecheckerplugin _CoqProject
 
 .merlin: Makefile.plugin
-	[ -e "src/pCUICsafecheckerplugin.ml" ] && make -f $< $@
+	make -f $< $@
 
 cleanplugin: Makefile.plugin
 	make -f Makefile.plugin clean

template-coq/Makefile

@@ -27,7 +27,7 @@ Makefile.template: _TemplateCoqProject
 	sed -e s/coqdeps/coqdeps.template/g Makefile.template > Makefile.template.tmp && mv -f Makefile.template.tmp Makefile.template
 
 .merlin: Makefile.plugin
-	[ -e "gen-src/signature.mli" ] && $(MAKE) -f $< $@
+	$(MAKE) -f $< $@
 
 coq: Makefile.coq
 	$(MAKE) -f Makefile.coq

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,

template-coq/src/run_template_monad.ml

@@ -281,8 +281,15 @@ let unquote_mutual_inductive_entry env evm trm (* of type mutual_inductive_entry
        in
        let priv = unquote_map_option unquote_bool priv in
        let ctx, univs = match univs with
-       | UState.Monomorphic_entry ctx ->
-          if template then Univ.ContextSet.empty, Entries.Template_ind_entry { univs = ctx; pseudo_sort_poly = TemplateUnivOnly }
+         | UState.Monomorphic_entry ctx ->
+           if template then
+             let mk_anon_names u =
+               let qs, us = UVars.Instance.to_array u in
+               Array.make (Array.length qs) Anonymous, Array.make (Array.length us) Anonymous
+             in
+             let uctx = UVars.UContext.of_context_set mk_anon_names Sorts.QVar.Set.empty ctx in
+             let default_univs = UVars.UContext.instance uctx in
+             Univ.ContextSet.empty, Entries.Template_ind_entry { uctx; default_univs }
           else ctx, Entries.Monomorphic_ind_entry
        | UState.Polymorphic_entry uctx -> Univ.ContextSet.empty, Entries.Polymorphic_ind_entry uctx
        in

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