From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Jan 2017 15:46:23 +0100 Subject: [location] Make location optional in Loc.located This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed and other times it printed nothing as the caller checked for `is_ghost` upstream. --- plugins/funind/indfun.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind/indfun.ml') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 1da85c467a..3dc16626ce 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -756,7 +756,7 @@ let rec add_args id new_args = Loc.map (function List.map (fun (b,na,b_option) -> add_args id new_args b, na, b_option) cel, - List.map (fun (loc,(cpl,e)) -> Loc.tag ~loc @@ (cpl,add_args id new_args e)) cal + List.map (fun (loc,(cpl,e)) -> Loc.tag ?loc @@ (cpl,add_args id new_args e)) cal ) | CLetTuple(nal,(na,b_option),b1,b2) -> CLetTuple(nal,(na,Option.map (add_args id new_args) b_option), @@ -882,7 +882,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalDef (na,_,_)-> [] | Constrexpr.CLocalAssum (nal,_,_) -> List.map - (fun (loc,n) -> Loc.tag ~loc @@ + (fun (loc,n) -> Loc.tag ?loc @@ CRef(Libnames.Ident(loc, Nameops.out_name n),None)) nal | Constrexpr.CLocalPattern _ -> assert false -- cgit v1.2.3