diff options
| author | Pierre-Marie Pédrot | 2018-04-13 12:49:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-04-13 12:49:54 +0200 |
| commit | f3b84cf63c242623bdcccd30c536e55983971da5 (patch) | |
| tree | 740984c577ed75c76edc2525b3de9bf744da3c21 /plugins/ssr/ssrcommon.ml | |
| parent | b68e0b4f9ba37d1c2fa5921e1d934b4b38bfdfe7 (diff) | |
| parent | 9f723f14e5342c1303646b5ea7bb5c0012a090ef (diff) | |
Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contains evars
Diffstat (limited to 'plugins/ssr/ssrcommon.ml')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d5118da4cb..e07bc48a47 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 = |