From dea62dfc660ffd61958c50e955f7b962afd83234 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 8 Sep 2015 12:03:04 +0200
Subject: Short cosmetic changes in tactics.ml.

---
 tactics/tactics.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f5d2bc3711..f2185d7dfe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -838,16 +838,15 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
   aux n []
 
 let get_next_hyp_position id gl =
-  let rec get_next_hyp_position id = function
+  let rec aux = function
   | [] -> raise (RefinerError (NoSuchHyp id))
   | (hyp,_,_) :: right ->
     if Id.equal hyp id then
       match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveLast
     else
-      get_next_hyp_position id right
+      aux right
   in
-  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-  get_next_hyp_position id hyps
+  aux (Proofview.Goal.hyps (Proofview.Goal.assume gl))
 
 let intro_replacing id =
   Proofview.Goal.enter begin fun gl ->
@@ -2255,7 +2254,7 @@ let ipat_of_name = function
   | Anonymous -> None
   | Name id -> Some (dloc, IntroNaming (IntroIdentifier id))
 
- let head_ident c =
+let head_ident c =
    let c = fst (decompose_app ((strip_lam_assum c))) in
    if isVar c then Some (destVar c) else None
 
-- 
cgit v1.2.3