diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal.ml | 5 | ||||
| -rw-r--r-- | proofs/proofview.ml | 5 |
2 files changed, 8 insertions, 2 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 1dd5be0e71..43a3024e50 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -89,7 +89,10 @@ module V82 = struct (* Instantiates a goal with an open term, using name of goal for evk' *) let partial_solution_to sigma evk evk' c = let id = Evd.evar_ident evk sigma in - Evd.rename evk' id (partial_solution sigma evk c) + let sigma = partial_solution sigma evk c in + match id with + | None -> sigma + | Some id -> Evd.rename evk' id sigma (* Parts of the progress tactical *) let same_goal evars1 gl1 evars2 gl2 = diff --git a/proofs/proofview.ml b/proofs/proofview.ml index ff8effcda4..8008b00253 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -1128,7 +1128,10 @@ struct | None -> Evd.define gl.Goal.self c sigma | Some evk -> let id = Evd.evar_ident gl.Goal.self sigma in - Evd.rename evk id (Evd.define gl.Goal.self c sigma) + let sigma = Evd.define gl.Goal.self c sigma in + match id with + | None -> sigma + | Some id -> Evd.rename evk id sigma in (** Restore the [future goals] state. *) let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in |