aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr/ssrcommon.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr/ssrcommon.ml')
-rw-r--r--plugins/ssr/ssrcommon.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index d5118da4c..e07bc48a4 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -504,7 +504,7 @@ let nf_evar sigma t =
EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr t))
let pf_abs_evars2 gl rigid (sigma, c0) =
- let c0 = EConstr.to_constr sigma c0 in
+ let c0 = EConstr.to_constr ~abort_on_undefined_evars:false sigma c0 in
let sigma0, ucst = project gl, Evd.evar_universe_context sigma in
let nenv = env_size (pf_env gl) in
let abs_evar n k =