Skip to content

Commit ba81528

Browse files
authored
Adapt to rocq-prover/rocq#21767 (qglobal is not qvar) (#214)
<!-- This is an auto-generated description by cubic. --> ## Summary by cubic Adapts Hammer to the latest `rocq` sort API from rocq-prover/rocq#21767 by replacing `QSort` with `GSort` and `VSort`; both map to `$Type` to preserve behavior. <sup>Written for commit 06fa3d2. Summary will update on new commits.</sup> <!-- End of auto-generated description by cubic. -->
1 parent bef16e0 commit ba81528

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)