* http://cs.unibo.it/helm/.
*)
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
type uri = string
type position = string
type depth = string
type spec = MustObj of uri list * position list * depth list
| MustSort of sort list * position list * depth list
- | MustRel of position list * depth list
- | OnlyObj of uri list * position list * depth list
+ | MustRel of position list * depth list
+ | OnlyObj of uri list * position list * depth list
| OnlySort of sort list * position list * depth list
- | OnlyRel of position list * depth list
- | Universe of position list
-
-type builtin_t = MainHypothesis
- | InHypothesis
- | MainConclusion
- | InConclusion
- | InBody
- | Set
- | Prop
- | Type
+ | OnlyRel of position list * depth list
+ | Universe of position list
val locate : string -> MathQL.query
val compose : spec list -> MathQL.query
-val builtin : builtin_t -> string
+val builtin : MathQL.vvar -> string
(* interface for the old constraints ***************************************)