From 20ee46f95d2198ea32750a7991ec9571c9eb2bb1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 12:00:02 +0200
Subject: Further SSR port.

---
 plugins/ssr/ssrequality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 1e4faa3eee..d52b83d529 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -625,7 +625,7 @@ let ssrinstancesofrule ist dir arg =
   Feedback.msg_info Pp.(str"BEGIN INSTANCES");
   try
     while true do
-      ignore(find env0 (EConstr.to_constr sigma0 concl0) 1 ~k:print)
+      ignore(find env0 (EConstr.to_constr ~abort_on_undefined_evars:false sigma0 concl0) 1 ~k:print)
     done; raise NoMatch
   with NoMatch -> Feedback.msg_info Pp.(str"END INSTANCES"); Tacticals.New.tclIDTAC
   end
-- 
cgit v1.2.3