diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 12 | ||||
| -rw-r--r-- | interp/constrintern.ml | 7 | ||||
| -rw-r--r-- | interp/impargs.ml | 2 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 4 | ||||
| -rw-r--r-- | interp/reserve.ml | 2 |
5 files changed, 13 insertions, 14 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f5eff693f..f1bee65ef 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1087,7 +1087,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t = (* Not "goal_concl_style" means do alpha-conversion avoiding only *) (* those goal/section/rel variables that occurs in the subterm under *) (* consideration; see namegen.ml for further details *) - let avoid = if goal_concl_style then ids_of_context env else [] in + let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype Detyping.Later ~lax:lax goal_concl_style avoid env sigma t in let vars = vars_of_env env in extern false (scopt,[]) vars r @@ -1099,14 +1099,14 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t = extern_constr_gen lax goal_concl_style None env sigma t let extern_type goal_concl_style env sigma t = - let avoid = if goal_concl_style then ids_of_context env else [] in + let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype Detyping.Later goal_concl_style avoid env sigma t in extern_glob_type (vars_of_env env) r let extern_sort sigma s = extern_glob_sort (detype_sort sigma s) let extern_closed_glob ?lax goal_concl_style env sigma t = - let avoid = if goal_concl_style then ids_of_context env else [] in + let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t in @@ -1177,15 +1177,15 @@ let rec glob_of_pat env sigma pat = DAst.make @@ match pat with | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.") in GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat) - | PFix f -> DAst.get (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *) - | PCoFix c -> DAst.get (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))) + | PFix f -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *) + | PCoFix c -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))) | PSort s -> GSort s let extern_constr_pattern env sigma pat = extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat) let extern_rel_context where env sigma sign = - let a = detype_rel_context Detyping.Later where [] (names_of_rel_context env,env) sigma sign in + let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in let vars = vars_of_env env in let a = List.map (extended_glob_local_binder_of_decl) a in pi3 (extern_local_binder (None,[]) vars a) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6f7c6c827..1cea307d7 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -469,8 +469,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio | _ -> assert false in let env = {env with ids = List.fold_right Id.Set.add il env.ids} in - let ienv = Id.Set.elements env.ids in - let id = Namegen.next_ident_away (Id.of_string "pat") ienv in + let id = Namegen.next_ident_away (Id.of_string "pat") env.ids in let na = (loc, Name id) in let bk = Default Explicit in let _, bl' = intern_assumption intern lvar env [na] bk tyc in @@ -1939,13 +1938,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | _ -> let fresh = Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in - canonize_args t tt (fresh::forbidden_names) + canonize_args t tt (Id.Set.add fresh forbidden_names) ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc) end | _ -> assert false in let _,args_rel = List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in - canonize_args args_rel l (Id.Set.elements forbidden_names_for_gen) [] [] in + canonize_args args_rel l forbidden_names_for_gen [] [] in match_to_do, Some (cases_pattern_expr_loc t,(ind,List.rev_map snd nal)) | None -> [], None in diff --git a/interp/impargs.ml b/interp/impargs.ml index d8241c044..09a0ba83c 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -255,7 +255,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = in match kind_of_term (whd_all env t) with | Prod (na,a,b) -> - let na',avoid = find_displayed_name_in all [] na ([],b) in + let na',avoid = find_displayed_name_in all Id.Set.empty na ([],b) in let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in !rigid, Array.to_list v | _ -> true, [] diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 3d48114ec..0967d21f0 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -577,7 +577,7 @@ let rec subst_notation_constr subst bound raw = if r1' == r1 && k' == k then raw else NCast(r1',k') let subst_interpretation subst (metas,pat) = - let bound = List.map fst metas in + let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in (metas,subst_notation_constr subst bound pat) (**********************************************************************) @@ -1143,7 +1143,7 @@ let rec match_ inner u alp metas sigma a1 a2 = to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *) | _b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner -> let avoid = - free_glob_vars a1 @ (* as in Namegen: *) glob_visible_short_qualid a1 in + Id.Set.union (free_glob_vars a1) (* as in Namegen: *) (glob_visible_short_qualid a1) in let id' = Namegen.next_ident_away id avoid in let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in let sigma = match t2 with diff --git a/interp/reserve.ml b/interp/reserve.ml index a1e5bd0ea..dc0f60dcf 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -110,7 +110,7 @@ let revert_reserved_type t = let t = EConstr.Unsafe.to_constr t in let reserved = KeyMap.find (constr_key t) !reserve_revtable in let t = EConstr.of_constr t in - let t = Detyping.detype Detyping.Now false [] (Global.env()) Evd.empty t in + let t = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _] then I've introduced a bug... *) let filter _ pat = |