diff options
| author | Arnaud Spiwack | 2014-10-13 18:26:05 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-16 10:37:40 +0200 |
| commit | 0ae6d27680e5b87bbb00c6941cee1b0c309624ec (patch) | |
| tree | ddc4f3477cc698ddd0284ca7d337027c2b5c97dd /tactics | |
| parent | 91f34a0a6744a06cb65c9ffe387f54f857a7bb28 (diff) | |
Goal: remove some functions from the compatibility layer.
The rest will take more work.
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) |