diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-13 17:36:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-13 17:51:34 +0100 |
| commit | 97e1fccd878190a1fc51a1da45f4c06369c0e3db (patch) | |
| tree | 27e38c1ae4c8ebef7dc7f8f893ccc8f93aee8227 /proofs | |
| parent | e9675e068f9e0e92bab05c030fb4722b146123b8 (diff) | |
| parent | f46a5686853353f8de733ae7fbd21a3a61977bc7 (diff) | |
Merge branch 'v8.5'
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 1dd5be0e7..43a3024e5 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 ff8effcda..8008b0025 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 |