Adapt w.r.t. coq/coq#16903.

lukaszcz · Jan 7, 2023 · 6abedf1 · 6abedf1
1 parent 82a0824
commit 6abedf1
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/plugin/hammer_main.ml b/src/plugin/hammer_main.ml
@@ -35,6 +35,7 @@ let hhterm_of_sort s = match Sorts.family s with
   | InProp -> mk_id "$Prop"
   | InSet  -> mk_id "$Set"
   | InType -> mk_id "$Type"
+  | InQSort -> mk_id "$Type"
 
 let hhterm_of_constant c =
   tuple [mk_id "$Const"; hhterm_of_global (Names.GlobRef.ConstRef c)]