diff options
| -rw-r--r-- | tactics/decl_proof_instr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index e4fa9cc9ef..bd3b8ab15e 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -649,7 +649,7 @@ let assume_st_letin hyps gls = (* suffices *) let free_meta info = - let max_next (i,_) j = if i <= j then succ j else i in + let max_next (i,_) j = if i >= j then succ i else j in List.fold_right max_next info.pm_subgoals 1 let rec metas_from n hyps = |