From 478ab43c9fe4ad87af59499e23a8051ad3561035 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 9 Nov 2023 16:33:12 +0100 Subject: [PATCH 1/2] Fix .merlin targets --- Makefile | 2 +- common/Makefile | 2 +- erasure-plugin/Makefile | 2 +- erasure/Makefile | 2 +- pcuic/Makefile | 2 +- quotation/Makefile | 2 +- safechecker/Makefile | 2 +- template-pcuic/Makefile | 2 +- utils/Makefile | 2 +- 9 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Makefile b/Makefile index cae917e41..fe782e77b 100644 --- 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 index ffb708a9f..128708724 100644 --- 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 index b408e3074..1953389f1 100644 --- 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 index ad1e14148..e61f05720 100644 --- 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 index cfaac23e4..c3359c694 100644 --- 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 index fe18b83ab..34cd87f21 100644 --- 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 index 69ab70cb2..8cf42221e 100644 --- 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-pcuic/Makefile b/template-pcuic/Makefile index 75c567db0..c8512874a 100644 --- 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 index b5014ff64..dd316847e 100644 --- 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 $< $@ From 0571a04570891960df52546ba064d86624090f5c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 9 Nov 2023 16:37:48 +0100 Subject: [PATCH 2/2] Adapt to coq/coq#18280 (case relevance outside case info) --- template-coq/src/denoter.ml | 4 ++-- template-coq/src/quoter.ml | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/template-coq/src/denoter.ml b/template-coq/src/denoter.ml index 221dd8bac..ce4642ed2 100644 --- 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 index 8889077f9..7e63684a5 100644 --- 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