Adapt to coq/coq#18981 (universe syntax change) (#15)

uds-psl · May 21, 2024 · 830b3d6 · 830b3d6
1 parent 957b255
commit 830b3d6
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/lib/gallinaGen.ml b/lib/gallinaGen.ml
@@ -16,8 +16,8 @@ let lident_ s = CAst.make (name_id_ s)
 let name_ s = Names.Name.mk_name (name_id_ s)
 
 let underscore_ = CAst.make Constrexpr.(CHole None)
-let prop_ = CAst.make Constrexpr.(CSort (Glob_term.UNamed (None,[CProp, 0])))
-let type_ = CAst.make Constrexpr.(CSort (Glob_term.UAnonymous { rigid = UnivRigid }))
+let prop_ = CAst.make Constrexpr.(CSort Constrexpr_ops.expr_Prop_sort)
+let type_ = CAst.make Constrexpr.(CSort Constrexpr_ops.expr_Type_sort)
 
 let app_ f xs =
   Constrexpr_ops.mkAppC (f, xs)