diff options
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 72d6cfbd2e..f7b7b607fd 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -72,6 +72,10 @@ let body_of_type ty = ty.body let incast_type tty = DOP2 (Cast, tty.body, (DOP0 (Sort tty.typ))) +let outcast_type = function + DOP2 (Cast, b, DOP0 (Sort s)) -> {body=b; typ=s} + | _ -> anomaly "outcast_type: Not an in-casted type judgement" + (****************************************************************************) (* Functions for dealing with constr terms *) (****************************************************************************) |