diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 344597fcd3..f8bca11558 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -40,7 +40,7 @@ let evars_to_goals p evm = let goals = ref Evar.Map.empty in let map ev evi = let evi, goal = p evm ev evi in - let () = if goal then goals := Evar.Map.add ev (Goal.V82.build ev) !goals in + let () = if goal then goals := Evar.Map.add ev ev !goals in evi in let evm = Evd.raw_map_undefined map evm in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index cd460ebbe7..f7c3c922fb 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1237,7 +1237,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let env = Environ.empty_env in let sigma = Evd.empty in let concl = Term.mkRel (-1) in - let goal = sig_it Goal.V82.dummy_goal in + let goal = Evar.unsafe_of_int (-1) in (* /dummy values *) let args = List.map (fun a -> snd(interp_genarg ist env sigma concl goal a)) l in catch_error_tac trace (tac args ist) |