aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr/ssrview.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr/ssrview.ml')
-rw-r--r--plugins/ssr/ssrview.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index aa614fbc1..afe03533d 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -254,7 +254,7 @@ let finalize_view s0 ?(simple_types=true) p =
Goal.enter_one ~__LOC__ begin fun g ->
let env = Goal.env g in
let sigma = Goal.sigma g in
- let evars_of_p = Evd.evars_of_term (EConstr.to_constr sigma p) in
+ let evars_of_p = Evd.evars_of_term (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in
let filter x _ = Evar.Set.mem x evars_of_p in
let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in
let p = Reductionops.nf_evar sigma p in