diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 9f0e47c6ce..f541698e98 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -937,7 +937,7 @@ let filter_possible_projections c ty ctxt args = List.map_i (fun i (id,b,_) -> let () = assert (i < len) in let a = Array.unsafe_get args i in - not (Option.is_empty b) || + (match b with None -> false | Some c -> not (isRel c || isVar c)) || a == c || (* Here we make an approximation, for instance, we could also be *) (* interested in finding a term u convertible to c such that a occurs *) |