diff options
| author | Hugo Herbelin | 2017-04-13 21:41:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-31 01:38:53 +0200 |
| commit | 8ab00e5f272aa8f16d70a00323c57f2d4ef66f03 (patch) | |
| tree | 337344749e72cc85334bfb56769272edf3e9b21d /interp/constrintern.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 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1d5d8e8658..b8d333f0d0 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -536,7 +536,7 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function try (* Binders bound in the notation are considered first-order objects *) let _,na = coerce_to_name (fst (Id.Map.find id terms)) in - (renaming,{env with ids = name_fold Id.Set.add na env.ids}), na + (renaming,{env with ids = Name.fold_right Id.Set.add na env.ids}), na with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) @@ -1660,7 +1660,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = | CCases (sty, rtnpo, tms, eqns) -> let as_in_vars = List.fold_left (fun acc (_,na,inb) -> Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc) - (Option.fold_left (fun acc (_,y) -> name_fold Id.Set.add y acc) acc na) + (Option.fold_left (fun acc (_,y) -> Name.fold_right Id.Set.add y acc) acc na) inb) Id.Set.empty tms in (* as, in & return vars *) let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in |