aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--tactics/class_tactics.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index f754a926d..2831e5ec3 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -321,7 +321,7 @@ let hints_tac hints =
| None -> gls', s'
| Some (evgls, s') ->
(* Reorder with dependent subgoals. *)
- (gls' @ List.map (fun (ev, x) -> Some ev, x) evgls, s')
+ (List.map (fun (ev, x) -> Some ev, x) evgls @ gls', s')
in
let gls' = list_map_i
(fun j (evar, g) ->