diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-13 21:41:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-31 01:38:53 +0200 |
| commit | 8ab00e5f272aa8f16d70a00323c57f2d4ef66f03 (patch) | |
| tree | 337344749e72cc85334bfb56769272edf3e9b21d /plugins/funind/indfun.ml | |
| parent | 4865160fa1f2e9ce03b37b9cb3ac99c35e9c4e4d (diff) | |
Creating a module Nameops.Name extending module Names.Name.
This module collects the functions of Nameops which are about Name.t
and somehow standardize or improve their name, resulting in particular
from discussions in working group.
Note the use of a dedicated exception rather than a failwith for
Nameops.Name.out.
Drawback of the approach: one needs to open Nameops, or to use long
prefix Nameops.Name.
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 74c0eb4cc..4946285e1 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -200,13 +200,13 @@ let is_rec names = | GIf(b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) | GProd(na,_,t,b) | GLambda(na,_,t,b) -> - lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b + lookup names t || lookup (Nameops.Name.fold_right Id.Set.remove na names) b | GLetIn(na,b,t,c) -> - lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c + lookup names b || Option.cata (lookup names) true t || lookup (Nameops.Name.fold_right Id.Set.remove na names) c | GLetTuple(nal,_,t,b) -> lookup names t || lookup (List.fold_left - (fun acc na -> Nameops.name_fold Id.Set.remove na acc) + (fun acc na -> Nameops.Name.fold_right Id.Set.remove na acc) names nal ) @@ -885,7 +885,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun (loc,n) -> CAst.make ?loc @@ - CRef(Libnames.Ident(loc, Nameops.out_name n),None)) + CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None)) nal | Constrexpr.CLocalPattern _ -> assert false ) |