diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-10 17:10:48 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:03 +0100 |
commit | 9324dcf528f16be420b08c376a6580c8987f50fd (patch) | |
tree | 21eda2f66226c0f9da6a9e6efd623048c4bb983d /interp | |
parent | 6b9a9124d3bd24fe9305df613547139f6f609c60 (diff) |
Using name given by user to name a 'pat, if any.
This works for contexts in Definition and co, but not yet for "fun" and co.
Diffstat (limited to 'interp')
-rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7276b917f..4658b6a33 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -461,7 +461,9 @@ 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 id = Namegen.next_ident_away (Id.of_string "pat") env.ids in + let na = alias_of_pat cp in + let ienv = Name.fold_right Id.Set.remove na env.ids in + let id = Namegen.next_name_away_with_default "pat" (alias_of_pat cp) ienv in let na = (loc, Name id) in let bk = Default Explicit in let _, bl' = intern_assumption intern lvar env [na] bk tyc in |