diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 4b5a6e01a8..0d2874cb76 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -49,8 +49,6 @@ let assumption_of_judgment env j = let sort_judgment env j = (type_judgment env j).utj_type -let on_judgment_type f j = { j with uj_type = f j.uj_type } - (************************************************) (* Incremental typing rules: builds a typing judgement given the *) (* judgements for the subterms. *) |