Cosmetic.

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 1c041d1eef8a1be882fbf2172cf42da7394f38c7..7dcd6417fc507b92698d92b467bb33053cbc5833 100644 (file)
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -45,8 +45,8 @@ let mk_elims (uri,_,_,_,obj) =
      let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
      let params = List.rev_map (function name,_ -> mk_id name) params in
      let args,sort = NCicReduction.split_prods ~subst:[] [] (-1) ty in
-     let rec_arg = mk_id (fresh_name ()) in
      let args = List.rev_map (function name,_ -> mk_id name) args in
+     let rec_arg = mk_id (fresh_name ()) in
      let p_ty =
       List.fold_right
        (fun name res -> CicNotationPt.Binder (`Forall,(name,None),res)) args
@@ -117,7 +117,6 @@ let mk_elims (uri,_,_,_,obj) =
          (function x::_ -> x | _ -> assert false)
          80 (CicNotationPres.render (Hashtbl.create 0)
          (TermContentPres.pp_ast res)));
-
       []
   | _ -> []
 ;;