From dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 3 May 2018 17:44:34 +0200
Subject: Remove some occurrences of Evd.empty

We address the easy ones, but they should probably be all removed.
---
 plugins/ssrmatching/ssrmatching.ml4 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/ssrmatching')

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 0dd3625ba2..93c63d522a 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -708,9 +708,9 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
 ;;
 
 
-let fixed_upat = function
+let fixed_upat evd = function
 | {up_k = KpatFlex | KpatEvar _ | KpatProj _} -> false 
-| {up_t = t} -> not (occur_existential Evd.empty (EConstr.of_constr t)) (** FIXME *)
+| {up_t = t} -> not (occur_existential evd (EConstr.of_constr t)) (** FIXME *)
 
 let do_once r f = match !r with Some _ -> () | None -> r := Some (f ())
 
@@ -769,7 +769,7 @@ let mk_tpattern_matcher ?(all_instances=false)
 let p2t p = mkApp(p.up_f,p.up_a) in 
 let source () = match upats_origin, upats with
   | None, [p] -> 
-      (if fixed_upat p then str"term " else str"partial term ") ++ 
+      (if fixed_upat ise p then str"term " else str"partial term ") ++
       pr_constr_pat (p2t p) ++ spc()
   | Some (dir,rule), [p] -> str"The " ++ pr_dir_side dir ++ str" of " ++ 
       pr_constr_pat rule ++ fnl() ++ ws 4 ++ pr_constr_pat (p2t p) ++ fnl()
-- 
cgit v1.2.3