diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3cf0c50ba..d9f857c4e 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -595,8 +595,8 @@ let filter_possible_projections c ty ctxt args = (* interested in finding a term u convertible to c such that a occurs *) (* in u *) isRel a && Int.Set.mem (destRel a) fv1 || - isVar a && Idset.mem (destVar a) fv2 || - Idset.mem id tyvars) + isVar a && Id.Set.mem (destVar a) fv2 || + Id.Set.mem id tyvars) ctxt args let solve_evars = ref (fun _ -> failwith "solve_evars not installed") |