diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-03 11:45:31 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-03 11:45:31 +0200 |
| commit | afe519db64b4864b5a901ab96a1e4297e9316b14 (patch) | |
| tree | 9fe22a04fcfd049081dedb6f9262a3a321176d03 /interp/constrintern.ml | |
| parent | e33cd69ab6fcb38478a6c0e00628a5de16181906 (diff) | |
| parent | b772c323f62b322c9b0a4ab90c7de8b1e2066bae (diff) | |
Merge PR #1040: Efficient fresh name generation
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 7 |
1 files changed, 3 insertions, 4 deletions
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 |