diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index ff280fa15f..e03d489c7f 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -328,7 +328,7 @@ let make_judge v tj = uj_type = tj } let j_val j = j.uj_val -let j_type j = body_of_type j.uj_type +let j_type j = j.uj_type type unsafe_type_judgment = { utj_val : constr; |