diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 10d9a1c4e..288eb9da2 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -230,7 +230,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let pretype_id loc env (lvar,unbndltacvars) id = try - let (n,typ) = lookup_rel_id id (rel_context env) in + let (n,_,typ) = lookup_rel_id id (rel_context env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> try |