let rec higher_name arity =
function
Cic.Sort Cic.Prop
- | Cic.Sort Cic.CProp ->
+ | Cic.Sort (Cic.CProp _) ->
if arity = 0 then "A" (* propositions *)
else if arity = 1 then "P" (* predicates *)
else "R" (*relations *)
in
(match ty with
C.Sort C.Prop
- | C.Sort C.CProp -> "H"
+ | C.Sort (C.CProp _) -> "H"
| _ -> guess_a_name context typ
)
with CicTypeChecker.TypeCheckerFailure _ -> "H"