From: Claudio Sacerdoti Coen Date: Fri, 15 May 2009 19:34:31 +0000 (+0000) Subject: Cosmetic. X-Git-Tag: make_still_working~3977 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f49690e1d1b39ccad40f1e874d9d19f6ffc289e0;p=helm.git Cosmetic. --- diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml index 1c041d1ee..7dcd6417f 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 @@ -117,7 +117,6 @@ let mk_elims (uri,_,_,_,obj) = (function x::_ -> x | _ -> assert false) 80 (CicNotationPres.render (Hashtbl.create 0) (TermContentPres.pp_ast res))); - [] | _ -> [] ;;