Merge pull request #1009 from SkySkimmer/ci-relevance

Adapt to coq/coq#18280 (case relevance outside case info)
MetaCoq · Nov 13, 2023 · 285a97a · 285a97a
2 parents 4b0d5da + 0571a04
commit 285a97a
Show file tree

Hide file tree

Showing 11 changed files with 13 additions and 13 deletions.
diff --git a/Makefile b/Makefile
@@ -128,7 +128,7 @@ mrproper:
 	$(MAKE) -C template-pcuic .merlin
 	$(MAKE) -C quotation .merlin
 	$(MAKE) -C erasure .merlin
-	$(MAKE) -C erasure-plugin .merin
+	$(MAKE) -C erasure-plugin .merlin
 
 utils:
 	$(MAKE) -C utils

diff --git a/common/Makefile b/common/Makefile
@@ -27,5 +27,5 @@ mrproper:
 Makefile.coq: _CoqProject
 	coq_makefile -f _CoqProject -o Makefile.coq
 
-.merlin:
+.merlin: Makefile.coq
 	$(MAKE) -f $< $@
diff --git a/erasure-plugin/Makefile b/erasure-plugin/Makefile
@@ -42,7 +42,7 @@ mrproper:
 	rm -f Makefile.erasureplugin _CoqProject
 
 .merlin: Makefile.plugin
-	[ -e "src/pCUICerasureplugin.ml" ] && make -f $< $@
+	make -f $< $@
 
 cleanplugin: Makefile.plugin
 	make -f Makefile.plugin clean

diff --git a/erasure/Makefile b/erasure/Makefile
@@ -22,7 +22,7 @@ clean: Makefile.erasure
 mrproper:
 	rm -f Makefile.erasure
 
-.merlin:
+.merlin: Makefile.erasure
 	make -f $< $@
 
 vos: Makefile.erasure

diff --git a/pcuic/Makefile b/pcuic/Makefile
@@ -27,7 +27,7 @@ mrproper:
 vos: Makefile.coq
 	$(MAKE) -f Makefile.coq vos
 
-.merlin:
+.merlin: Makefile.coq
 	$(MAKE) -f $< $@
 
 quick: Makefile.coq

diff --git a/quotation/Makefile b/quotation/Makefile
@@ -23,7 +23,7 @@ mrproper:
 	rm -f metacoq-config
 	rm -f Makefile.quotation _CoqProject
 
-.merlin:
+.merlin: Makefile.quotation
 	make -f $< $@
 
 vos: Makefile.quotation

diff --git a/safechecker/Makefile b/safechecker/Makefile
@@ -23,7 +23,7 @@ mrproper:
 	rm -f metacoq-config
 	rm -f Makefile.safechecker _CoqProject
 
-.merlin:
+.merlin: Makefile.safechecker
 	make -f $< $@
 
 vos: Makefile.safechecker

diff --git a/template-coq/src/denoter.ml b/template-coq/src/denoter.ml
@@ -108,7 +108,7 @@ struct
       | ACoq_tCase (ci, p, c, brs) ->
         let ind = D.unquote_inductive ci.aci_ind in
         let relevance = D.unquote_relevance ci.aci_relevance in 
-        let ci = Inductiveops.make_case_info (Global.env ()) ind relevance Constr.RegularStyle in
+        let ci = Inductiveops.make_case_info (Global.env ()) ind Constr.RegularStyle in
         let evm, puinst = D.unquote_universe_instance evm p.auinst in
         let evm, pars = map_evm (aux env) evm p.apars in
         let pars = Array.of_list pars in
@@ -126,7 +126,7 @@ struct
         in
         let evm, brs = array_map_evm denote_br evm brs in
         (* todo: reify better case_info *)
-        let pcase = (ci, puinst, pars, (napctx, pret), Constr.NoInvert, c, brs) in
+        let pcase = (ci, puinst, pars, ((napctx, pret), relevance), Constr.NoInvert, c, brs) in
         evm, Constr.mkCase pcase
       | ACoq_tFix (lbd, i) ->
         let (names,types,bodies,rargs) = (List.map (fun p->p.adname) lbd,  List.map (fun p->p.adtype) lbd, List.map (fun p->p.adbody) lbd,

diff --git a/template-coq/src/quoter.ml b/template-coq/src/quoter.ml
@@ -314,11 +314,11 @@ struct
           let mib = Environ.lookup_mind (fst mind) (snd env) in
           add_inductive mind mib acc)
 
-      | Constr.Case (ci,u,pars, (predctx, pred), iv, discr, brs) ->
+      | Constr.Case (ci,u,pars, ((predctx, pred), relevance), iv, discr, brs) ->
         let ind = Q.quote_inductive (Q.quote_kn (Names.MutInd.canonical (fst ci.Constr.ci_ind)),
                                       Q.quote_int (snd ci.Constr.ci_ind)) in
         let npar = Q.quote_int ci.Constr.ci_npar in
-        let q_relevance = Q.quote_relevance ci.Constr.ci_relevance in
+        let q_relevance = Q.quote_relevance relevance in
         let acc, q_pars = CArray.fold_left_map (fun acc par -> let (qt, acc) = quote_term acc env sigma par in acc, qt) acc pars in 
         let qu = Q.quote_univ_instance u in
         let pctx = CaseCompat.case_predicate_context (snd env) ci u pars predctx in 

diff --git a/template-pcuic/Makefile b/template-pcuic/Makefile
@@ -23,7 +23,7 @@ mrproper:
 	rm -f metacoq-config
 	rm -f Makefile.templatepcuic _CoqProject
 
-.merlin:
+.merlin: Makefile.templatepcuic
 	make -f $< $@
 
 vos: Makefile.templatepcuic

diff --git a/utils/Makefile b/utils/Makefile
@@ -23,5 +23,5 @@ mrproper:
 Makefile.coq: _CoqProject
 	coq_makefile -f _CoqProject -o Makefile.coq
 
-.merlin:
+.merlin: Makefile.coq
 	$(MAKE) -f $< $@