Skip to content

Commit 598ec5a

Browse files
authored
Merge pull request #1240 from SkySkimmer/match-style
Adapt to rocq-prover/rocq#21646 (RegularStyle := MatchStyle)
2 parents e8f8078 + dfb4659 commit 598ec5a

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

template-rocq/src/denoter.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,7 @@ struct
112112
| ACoq_tCase (ci, p, c, brs) ->
113113
let ind = D.unquote_inductive ci.aci_ind in
114114
let relevance = D.unquote_relevance ci.aci_relevance in
115-
let ci = Inductiveops.make_case_info (Global.env ()) ind Constr.RegularStyle in
115+
let ci = Inductiveops.make_case_info (Global.env ()) ind Constr.MatchStyle in
116116
let evm, puinst = D.unquote_universe_instance evm p.auinst in
117117
let evm, pars = map_evm (aux env) evm p.apars in
118118
let pars = Array.of_list pars in

0 commit comments

Comments
 (0)