From f49690e1d1b39ccad40f1e874d9d19f6ffc289e0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 15 May 2009 19:34:31 +0000 Subject: [PATCH] Cosmetic. --- helm/software/components/ng_tactics/nCicElim.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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))); - [] | _ -> [] ;; -- 2.39.2