diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 3563c77887..40599f4a35 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1015,6 +1015,7 @@ let is_unification_pattern_evar env (_,args) l t = l else (* Probably strong restrictions coming from t being evar-closed *) + let t = expand_vars_in_term env t in let fv_rels = free_rels t in let fv_ids = global_vars env t in List.filter (fun c -> |