diff options
| author | Pierre-Marie Pédrot | 2020-05-01 12:00:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-03 13:09:50 +0200 |
| commit | 20ee46f95d2198ea32750a7991ec9571c9eb2bb1 (patch) | |
| tree | 08d7939f88d15f8b2fe05688f690d0f61f84262d /plugins/ssr | |
| parent | f13c800114b8cf378fe7d52757d310923a46737e (diff) | |
Further SSR port.
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 2 |
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 |