diff options
Diffstat (limited to 'proofs/goal.ml')
| -rw-r--r-- | proofs/goal.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index ef71dd04c..fe8018e47 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -81,12 +81,17 @@ module V82 = struct (* Instantiates a goal with an open term *) let partial_solution sigma evk c = + (* Check that the goal itself does not appear in the refined term *) + let _ = + if not (Evarutil.occur_evar_upto sigma evk c) then () + else Pretype_errors.error_occur_check Environ.empty_env sigma evk c + in Evd.define evk c sigma (* 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 (Evd.define evk c sigma) + Evd.rename evk' id (partial_solution sigma evk c) (* Parts of the progress tactical *) let same_goal evars1 gl1 evars2 gl2 = |