aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrequality.ml2
1 files changed, 1 insertions, 1 deletions
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