diff options
| author | coqbot-app[bot] | 2020-08-25 08:32:20 +0000 |
|---|---|---|
| committer | GitHub | 2020-08-25 08:32:20 +0000 |
| commit | bd4791ff350bef9dc45b42b2ae77769625644c4f (patch) | |
| tree | 02fb8f7c029ea53839714688edd8b888af9a3db8 /vernac | |
| parent | 016bafd7519859737610810df77f72bf812c542a (diff) | |
| parent | a970072a64348a1b5af1cd45a138da819ef0a8d2 (diff) | |
Merge PR #12878: Update sigma instead of erasing it in `update_global_env`
Reviewed-by: SkySkimmer
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 |