diff options
| author | Maxime Dénès | 2017-06-01 15:44:11 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-01 15:44:11 +0200 |
| commit | 84d49e38a245cbbbe5b6111a4e4d9afcbac2d33b (patch) | |
| tree | 0e6bff9cf7c2aaf6967352bd5b5f8c8a2831a570 /interp/constrintern.ml | |
| parent | 48621da27d52be4825eea271d44bbd7362011dfa (diff) | |
| parent | 8ab00e5f272aa8f16d70a00323c57f2d4ef66f03 (diff) | |
Merge PR#561: Improving the Name API
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6514ad8be5..81ebf65610 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 @@ -2071,7 +2071,7 @@ let intern_context global_level env impl_env binders = with InternalizationError (loc,e) -> user_err ?loc ~hdr:"internalize" (explain_internalization_error e) -let interp_rawcontext_evars env evdref k bl = +let interp_glob_context_evars env evdref k bl = let open EConstr in let (env, par, _, impls) = List.fold_left @@ -2100,6 +2100,6 @@ let interp_rawcontext_evars env evdref k bl = let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params = let int_env,bl = intern_context global_level env impl_env params in - let x = interp_rawcontext_evars env evdref shift bl in + let x = interp_glob_context_evars env evdref shift bl in int_env, x |