diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-18 15:46:23 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-25 00:28:53 +0200 |
| commit | e8a6467545c2814c9418889201e8be19c0cef201 (patch) | |
| tree | 7f513d854b76b02f52f98ee0e87052c376175a0f /pretyping/glob_ops.ml | |
| parent | 30d3515546cf244837c6340b6b87c5f51e68cbf4 (diff) | |
[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 <unknown> 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 <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
Diffstat (limited to 'pretyping/glob_ops.ml')
| -rw-r--r-- | pretyping/glob_ops.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index cba1780ba..7e6b063d0 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -354,7 +354,7 @@ let add_and_check_ident id set = Id.Set.add id set let bound_glob_vars = - let rec vars bound = Loc.with_loc (fun ~loc -> function + let rec vars bound = Loc.with_loc (fun ?loc -> function | GLambda (na,_,_,_) | GProd (na,_,_,_) | GLetIn (na,_,_,_) as c -> let bound = name_fold add_and_check_ident na bound in fold_glob_constr vars bound (loc, c) @@ -495,7 +495,7 @@ let rename_var l id = if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming else id -let rec rename_glob_vars l = Loc.map_with_loc (fun ~loc -> function +let rec rename_glob_vars l = Loc.map_with_loc (fun ?loc -> function | GVar id as r -> let id' = rename_var l id in if id == id' then r else GVar id' @@ -558,10 +558,10 @@ let rec cases_pattern_of_glob_constr na = Loc.map (function ) (* Turn a closed cases pattern into a glob_constr *) -let rec glob_constr_of_closed_cases_pattern_aux x = Loc.map_with_loc (fun ~loc -> function +let rec glob_constr_of_closed_cases_pattern_aux x = Loc.map_with_loc (fun ?loc -> function | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None) | PatCstr (cstr,l,Anonymous) -> - let ref = Loc.tag ~loc @@ GRef (ConstructRef cstr,None) in + let ref = Loc.tag ?loc @@ GRef (ConstructRef cstr,None) in GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l) | _ -> raise Not_found ) x |