| T.InBody -> ns ^ "InBody"
let string_of_sort = function
- | T.Set -> "Set"
- | T.Prop -> "Prop"
- | T.Type -> "Type"
+ | T.Set -> "Set"
+ | T.Prop -> "Prop"
+ | T.Type -> "Type"
+ | T.CProp -> "CProp"
let string_of_depth = string_of_int
| T.InBody -> "$IB"
let mathql_of_sort = function
- | T.Set -> "$SET"
- | T.Prop -> "$PROP"
- | T.Type -> "$TYPE"
+ | T.Set -> "$SET"
+ | T.Prop -> "$PROP"
+ | T.Type -> "$TYPE"
+ | T.CProp -> "$CPROP"
let mathql_of_depth = string_of_int
| _ -> raise Parsing.Parse_error
let sort_of_mathql = function
- | "$SET" -> T.Set
- | "$PROP" -> T.Prop
- | "$TYPE" -> T.Type
+ | "$SET" -> T.Set
+ | "$PROP" -> T.Prop
+ | "$TYPE" -> T.Type
+ | "$CPROP" -> T.CProp
| _ -> raise Parsing.Parse_error
let depth_of_mathql s =
| _ -> no_depth_text
let text_of_sort = function
- | T.Set -> "Set"
- | T.Prop -> "Prop"
- | T.Type -> "Type"
+ | T.Set -> "Set"
+ | T.Prop -> "Prop"
+ | T.Type -> "Type"
+ | T.CProp -> "CProp"
let is_main_position = function
| `MainHypothesis _
let set_main_position pos depth = match pos with
| `MainHypothesis _ -> `MainHypothesis depth
| `MainConclusion _ -> `MainConclusion depth
-
-let universe_for_search_pattern =
- [T.MainHypothesis; T.InHypothesis; T.MainConclusion; T.InConclusion]
-
-let universe_for_match_conclusion = [T.MainConclusion; T.InConclusion]