- let u2 =
- match u2 with
- | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
- NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
- | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
- NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
- | _ -> raise (Failure "only a sort can be constrained")
- in
- G.NUnivConstraint (loc, strict,u1,u2)