Useless use of maps in constr internalizing.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16607 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 5 insertions, 4 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index cfb96b488f..e75c5dd46c 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -302,7 +302,7 @@ let intern_binding_name ist x =
 let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
   let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
   let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in
-  let ltacvars = (fst lfun, Id.Map.empty) in
+  let ltacvars = (fst lfun, Id.Set.empty) in
   let c' =
     warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars sigma env) c
   in
@@ -441,11 +441,11 @@ let intern_hyp_location ist ((occs,id),hl) =
 (* Reads a pattern *)
 let intern_pattern ist ?(as_type=false) lfun = function
   | Subterm (b,ido,pc) ->
-      let ltacvars = (lfun, Id.Map.empty) in
+      let ltacvars = (lfun, Id.Set.empty) in
       let (metas,pc) = intern_constr_pattern ist ltacvars pc in
       ido, metas, Subterm (b,ido,pc)
   | Term pc ->
-      let ltacvars = (lfun, Id.Map.empty) in
+      let ltacvars = (lfun, Id.Set.empty) in
       let (metas,pc) = intern_constr_pattern ist ltacvars pc in
       None, metas, Term pc
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 7158ddf7ed..09dcb49f40 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -465,7 +465,8 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   | Some c ->
       let fold id _ accu = id :: accu in
       let ltacvars = Id.Map.fold fold constrvars [] in
-      let ltacdata = (ltacvars, ist.lfun) in
+      let bndvars = Id.Map.fold (fun x _ accu -> Id.Set.add x accu) ist.lfun Id.Set.empty in
+      let ltacdata = (ltacvars, bndvars) in
       intern_gen kind ~allow_patvar ~ltacvars:ltacdata sigma env c
   in
   let trace =