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

5 files changed, 10 insertions, 9 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ec8794e468..2adeb27cc5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -632,7 +632,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
   else if Id.equal id ldots_var
   then
     if ntnvars != [] then GVar (loc,id), [], [], [] else error_ldots_var loc
-  else if Id.Map.mem id unbndltacvars then
+  else if Id.Set.mem id unbndltacvars then
     (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
     user_err_loc (loc,"intern_var",
       str "variable " ++ pr_id id ++ str " should be bound to a term.")
@@ -1659,9 +1659,9 @@ let scope_of_type_kind = function
   | OfType typ -> compute_type_scope typ
   | WithoutTypeConstraint -> None
 
-type ltac_sign = Id.t list * unbound_ltac_var_map
+type ltac_sign = Id.t list * Id.Set.t
 
-let empty_ltac_sign = ([], Id.Map.empty)
+let empty_ltac_sign = ([], Id.Set.empty)
 
 let intern_gen kind sigma env
                ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 32e878165c..2a80856827 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -68,7 +68,7 @@ val compute_internalization_env : env -> var_internalization_type ->
   Id.t list -> types list -> Impargs.manual_explicitation list list ->
   internalization_env
 
-type ltac_sign = Id.t list * unbound_ltac_var_map
+type ltac_sign = Id.t list * Id.Set.t
 
 type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 44fd838319..6c75e84154 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -132,7 +132,7 @@ let rec abstract_glob_constr c = function
 
 let interp_casted_constr_with_implicits sigma env impls c  =
   Constrintern.intern_gen Pretyping.WithoutTypeConstraint sigma env ~impls
-    ~allow_patvar:false  ~ltacvars:([],Id.Map.empty) c
+    ~allow_patvar:false  ~ltacvars:([],Id.Set.empty) c
 
 (*
    Construct a fixpoint as a Glob_term
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 =