diff options
Diffstat (limited to 'tactics/decl_proof_instr.ml')
| -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 74ffc0a9c..a8d2fb950 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -752,7 +752,7 @@ let rec consider_match may_intro introduced available expected gls = consider_match may_intro ((id,false)::introduced) rest_ids rest | Name hid -> tclTHENLIST - [rename_hyp id hid; + [rename_hyp [id,hid]; consider_match may_intro ((hid,true)::introduced) rest_ids rest] end begin |