diff options
| author | Pierre-Marie Pédrot | 2020-10-07 12:15:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-07 12:15:41 +0200 |
| commit | 51c1b467829f4be4fd9192d7d55fb28915e0ac04 (patch) | |
| tree | a5ff34a96b6717acd953c503de62802c504d3ad4 /plugins | |
| parent | ab70eb09c69a2b21556329e863e4235d304f2e89 (diff) | |
| parent | 5135153d6cd2f22a82dd7209f46c02ed3f7c78cb (diff) | |
Merge PR #13115: Derive Inversion does not allow leftover evars
Reviewed-by: ppedrot
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/leminv.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml index 47df3ec34f..f42c1f73a3 100644 --- a/plugins/ltac/leminv.ml +++ b/plugins/ltac/leminv.ml @@ -245,7 +245,8 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let add_inversion_lemma_exn ~poly na com comsort bool tac = let env = Global.env () in let sigma = Evd.from_env env in - let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in + let c, uctx = Constrintern.interp_type env sigma com in + let sigma = Evd.from_ctx uctx in let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in add_inversion_lemma ~poly na env sigma c sort bool tac |