The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

On Fri, 5 Feb 2021 15:32:49 -0500
"jonikelee AT gmail.com" <jonikelee AT gmail.com> wrote:

> Is it possible for an Ltac or Ltac2 tactic to check if one sort A is
> a subtype of another sort B (an existing i<=j constraint between
> sorts A=Type@{i} and B=Type{j}) without adding any new universe
> constraints?

I think I figured it out - the trick is to use backtracking on success
to undo added constraints:

Ltac issubtype A B := (*assumes A and B are both sorts*)
  first [constr_eq_strict A B
        |let _:=constr:(B:A) in fail 1 "B is constrained <= A"
        |let tA:=type of A in
         let _:=constr:(B:tA) in fail 1 "A and B might be siblings"
        |assert_succeeds (let _:=constr:(A:B) in idtac)
        ].