diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/declare.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/vernac/declare.ml b/vernac/declare.ml index 66537c2978..28e6f21d41 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1735,11 +1735,7 @@ let return_proof ps = List.map (fun (((_ub, body),eff),_) -> (body,eff)) p, uctx let update_global_env = - map ~f:(fun p -> - let { Proof.sigma } = Proof.data p in - let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in - let p, (status,info), _ = Proof.run_tactic (Global.env ()) tac p in - p) + map ~f:(fun p -> Proof.update_sigma_env p (Global.env ())) let next = let n = ref 0 in fun () -> incr n; !n |