diff options
| author | Enrico Tassi | 2020-08-19 11:17:49 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2020-08-19 11:17:49 +0200 |
| commit | ae38c38837e068721cc54d01570427aefdce49c5 (patch) | |
| tree | 69adbd7922a6bc52f0758b8eca0095778f64c1d5 /plugins | |
| parent | daed771ff18978dea536b277e00c0ca0149129ee (diff) | |
| parent | 2edad4e3903ee77155f8b164c6cf6df49c897a27 (diff) | |
Merge PR #12725: Store evar identity instances in evarinfo / named_context_val
Ack-by: SkySkimmer
Reviewed-by: gares
Diffstat (limited to 'plugins')
| -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 1b7768852e..d7996a722a 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1352,7 +1352,7 @@ let unsafe_intro env decl b = Refine.refine ~typecheck:false begin fun sigma -> let ctx = Environ.named_context_val env in let nctx = EConstr.push_named_context_val decl ctx in - let inst = List.map (get_id %> EConstr.mkVar) (Environ.named_context env) in + let inst = EConstr.identity_subst_val (Environ.named_context_val env) in let ninst = EConstr.mkRel 1 :: inst in let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in let sigma, ev = Evarutil.new_pure_evar ~principal:true nctx sigma nb in |