diff options
| author | Emilio Jesus Gallego Arias | 2020-07-08 12:32:00 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-07-08 12:32:00 +0200 |
| commit | cf383c1f2e0c9effd9774bc25579eeaca4c24ae0 (patch) | |
| tree | 229f3c6023d32b09cc646ce28497f91d096cb87e /plugins | |
| parent | 5331a010acbb71131bc5dc1c62cc08d9814de21b (diff) | |
| parent | 834c64015b608b8152e160d37e6f07a3106ff26b (diff) | |
Merge PR #12645: Cleanup Evarutil API
Reviewed-by: ejgallego
Reviewed-by: herbelin
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 5f463f8de4..65204b7868 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1351,9 +1351,8 @@ let unsafe_intro env decl b = let inst = List.map (get_id %> EConstr.mkVar) (Environ.named_context 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_evar_instance nctx sigma nb ~principal:true ninst in - sigma, EConstr.mkNamedLambda_or_LetIn decl ev + let sigma, ev = Evarutil.new_pure_evar ~principal:true nctx sigma nb in + sigma, EConstr.mkNamedLambda_or_LetIn decl (EConstr.mkEvar (ev, ninst)) end let set_decl_id id = let open Context in function |
