From 7126990e5b04d51927f414b277124c127fb14887 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 13 Jul 2020 15:02:43 +0200
Subject: Actually use the default instance stored inside named_context_val.

---
 plugins/ssr/ssrcommon.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

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
-- 
cgit v1.2.3