X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnCicElim.ml;h=fba21753a53ce6ef8b749839b716020ca7b702e8;hb=72cd94b68037956a70b98cfa54f316fd54e52bae;hp=1c041d1eef8a1be882fbf2172cf42da7394f38c7;hpb=4e98c439731c6e110430a6c5217274215bf403b6;p=helm.git

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 1c041d1ee..fba21753a 100644
--- 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)));
-
       []
   | _ -> []
 ;;