From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 30 Oct 2016 17:53:07 +0100 Subject: Termops API using EConstr. --- plugins/ssrmatching/ssrmatching.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ssrmatching') 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 ()) -- cgit v1.2.3