repeat_tac

[helm.git] / helm / software / components / ng_tactics / nCicElim.ml

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 1c041d1eef8a1be882fbf2172cf42da7394f38c7..fba21753a53ce6ef8b749839b716020ca7b702e8 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
@@ -115,9 +115,8 @@ let mk_elims (uri,_,_,_,obj) =
        (BoxPp.render_to_string
          ~map_unicode_to_tex:false
          (function x::_ -> x | _ -> assert false)
-         80 (CicNotationPres.render (Hashtbl.create 0)
+         80 (CicNotationPres.render (fun _ -> None)
          (TermContentPres.pp_ast res)));
-
       []
   | _ -> []
 ;;