diff options
| author | Emilio Jesus Gallego Arias | 2019-07-01 04:00:11 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-11 18:19:12 +0200 |
| commit | 2576fee1798b753161a730244c8d4d701e8a4641 (patch) | |
| tree | e07fa6b7e015b08565fd73c9f36c4dcf8cc2cfed /user-contrib | |
| parent | efe7108a0ae32faeb674cc5d97e6fa955a1dccd8 (diff) | |
[proof] Minor cleanup in proof.ml
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 3b8fc58c6f..17004bb012 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -763,7 +763,7 @@ let perform_eval ~pstate e = | Goal_select.SelectAlreadyFocused -> assert false (* TODO **) in let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in - let sigma = Proof.in_proof proof (fun sigma -> sigma) in + let { Proof.sigma } = Proof.data proof in let name = int_name () in Feedback.msg_notice (str "- : " ++ pr_glbtype name (snd ty) ++ spc () ++ str "=" ++ spc () ++ |