Skip to content

Commit 06fa3d2

Browse files
committed
Adapt to rocq-prover/rocq#21767 (qglobal is not qvar)
1 parent bef16e0 commit 06fa3d2

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

src/plugin/hammer_main.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ let hhterm_of_sort s = match s with
3535
| Prop -> mk_id "$Prop"
3636
| Set -> mk_id "$Set"
3737
| Type _ -> mk_id "$Type"
38-
| QSort _ -> mk_id "$Type"
38+
| GSort _ | VSort _ -> mk_id "$Type"
3939

4040
let hhterm_of_constant c =
4141
tuple [mk_id "$Const"; hhterm_of_global (Names.GlobRef.ConstRef c)]

0 commit comments

Comments
 (0)