diff options
| author | Hugo Herbelin | 2015-01-05 06:42:37 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-01-06 14:19:13 +0100 |
| commit | f1db73816e4bd463cc81f34ba7e35857694bfa25 (patch) | |
| tree | 090d244562a10e5f57b7b80f1c79c2170e8bef31 | |
| parent | ba92fdf0422503d7b69c3cd02d67a4dcee408d64 (diff) | |
Propagating the relaxing of filtering started in 48509b6, fixed in
3cd718c, to the case of second_order_matching.
| -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 *) |