Skip to content

Commit 922d1e1

Browse files
authored
Merge pull request #1201 from ppedrot/environ-store-canonical-mapping
Adapt to rocq-prover/rocq#21049.
2 parents 44c804a + 9d6279e commit 922d1e1

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

template-rocq/src/denoter.ml

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -98,7 +98,9 @@ struct
9898
| ACoq_tConst (s,u) ->
9999
let s = D.unquote_kn s in
100100
let evm, u = D.unquote_universe_instance evm u in
101-
evm, Constr.mkConstU (Constant.make1 s, u)
101+
(* XXX use the Environ API when available *)
102+
let cst = Global.constant_of_delta_kn s in
103+
evm, Constr.mkConstU (cst, u)
102104
| ACoq_tConstruct (i,idx,u) ->
103105
let ind = D.unquote_inductive i in
104106
let evm, u = D.unquote_universe_instance evm u in

0 commit comments

Comments
 (0)