- strict = [ SYMBOL <:unicode<lt>> -> true
- | SYMBOL <:unicode<leq>> -> false ];
- u2 = tactic_term ->
- let u1 =
- match u1 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
- let u2 =
- match u2 with