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.

3 files changed, 14 insertions, 1 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7276b917fa..4658b6a33a 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
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 6b09c33084..8a6d94c732 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -39,3 +39,9 @@ forall '(x, y) '(z, t), swap (x, y) = (z, t)
      : Prop
 fun (pat : nat) '(x, y) => x + y = pat
      : nat -> nat * nat -> Prop
+f = fun x : nat => x + x
+     : nat -> nat
+
+Argument scope is [nat_scope]
+fun x : nat => x + x
+     : nat -> nat
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index 0bad472f41..d671053c07 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -67,3 +67,8 @@ End Suboptimal.
 
 (** Test risk of collision for internal name *)
 Check fun pat => fun '(x,y) => x+y = pat.
+
+(** Test name in degenerate case *)
+Definition f 'x := x+x.
+Print f.
+Check fun 'x => x+x.