Skip to content

Commit 5544fb9

Browse files
authored
Merge pull request MetaRocq#1231 from JasonGross/print-assumptions-list
Adapt to rocq-prover/rocq#21477 (`Print Assumptions` takes list)
2 parents 0041aaa + e7fb3dc commit 5544fb9

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

safechecker-plugin/src/g_metarocq_safechecker.mlg

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ let retypecheck_term_dependencies ~opaque_access env gr =
7575
in
7676
let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in
7777
let deps = Assumptions.assumptions ~add_opaque:true ~add_transparent:true opaque_access
78-
st gr (fst (UnivGen.fresh_global_instance env gr)) in
78+
st [gr] in
7979
let process_object k _ty =
8080
let open Printer in
8181
match k with

0 commit comments

Comments
 (0)