aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssrmatching/ssrmatching.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssrmatching/ssrmatching.ml4')
-rw-r--r--plugins/ssrmatching/ssrmatching.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 77e25b2a5..86cc928c8 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -702,7 +702,7 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
let fixed_upat = function
| {up_k = KpatFlex | KpatEvar _ | KpatProj _} -> false
-| {up_t = t} -> not (occur_existential t)
+| {up_t = t} -> not (occur_existential Evd.empty (EConstr.of_constr t)) (** FIXME *)
let do_once r f = match !r with Some _ -> () | None -> r := Some (f ())