diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-13 18:26:05 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 10:37:40 +0200 |
| commit | 0ae6d27680e5b87bbb00c6941cee1b0c309624ec (patch) | |
| tree | ddc4f3477cc698ddd0284ca7d337027c2b5c97dd /tactics/class_tactics.ml | |
| parent | 91f34a0a6744a06cb65c9ffe387f54f857a7bb28 (diff) | |
Goal: remove some functions from the compatibility layer.
The rest will take more work.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 344597fcd..f8bca1155 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 |