Replacing an association list by a map in globalizing environment.

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

6 files changed, 19 insertions, 15 deletions

diff --git a/interp/genintern.ml b/interp/genintern.ml
index d7171a4d15..86a1ce1f5d 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -14,7 +14,7 @@ open Genarg
 
 type glob_sign = {
   ltacvars : Id.Set.t;
-  ltacrecvars : (Id.t * Nametab.ltac_constant) list;
+  ltacrecvars : Nametab.ltac_constant Id.Map.t;
   gsigma : Evd.evar_map;
   genv : Environ.env }
 
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 9fe553cbaa..7027315e76 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -12,7 +12,7 @@ open Genarg
 
 type glob_sign = {
   ltacvars : Id.Set.t;
-  ltacrecvars : (Id.t * Nametab.ltac_constant) list;
+  ltacrecvars : Nametab.ltac_constant Id.Map.t;
   gsigma : Evd.evar_map;
   genv : Environ.env }
 
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index cabbd4755d..a06b44083d 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1459,7 +1459,7 @@ let do_instr raw_instr pts =
       let { it=gls ; sigma=sigma } = Proof.V82.subgoals pts in
       let gl = { it=List.hd gls ; sigma=sigma } in
       let env=  pf_env gl in
-      let ist = {ltacvars = Id.Set.empty; ltacrecvars = [];
+      let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
 		 gsigma = sigma; genv = env} in
       let glob_instr = intern_proof_instr ist raw_instr in
       let instr =
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 503888c380..eca9c7716c 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -55,13 +55,13 @@ let skip_metaid = function
 type glob_sign = Genintern.glob_sign = {
   ltacvars : Id.Set.t;
      (* ltac variables and the subset of vars introduced by Intro/Let/... *)
-  ltacrecvars : (Id.t * ltac_constant) list;
+  ltacrecvars : ltac_constant Id.Map.t;
      (* ltac recursive names *)
   gsigma : Evd.evar_map;
   genv : Environ.env }
 
 let fully_empty_glob_sign =
-  { ltacvars = Id.Set.empty; ltacrecvars = [];
+  { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
     gsigma = Evd.empty; genv = Environ.empty_env }
 
 let make_empty_glob_sign () =
@@ -126,7 +126,7 @@ let find_ident id ist =
   Id.Set.mem id ist.ltacvars ||
   List.mem id (ids_of_named_context (Environ.named_context ist.genv))
 
-let find_recvar qid ist = List.assoc qid ist.ltacrecvars
+let find_recvar qid ist = Id.Map.find qid ist.ltacrecvars
 
 (* a "var" is a ltac var or a var introduced by an intro tactic *)
 let find_var id ist = Id.Set.mem id ist.ltacvars
@@ -806,7 +806,7 @@ let glob_tactic_env l env x =
     List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
   Flags.with_option strict_check
   (intern_pure_tactic
-    { ltacvars; ltacrecvars = []; gsigma = Evd.empty; genv = env })
+    { ltacvars; ltacrecvars = Id.Map.empty; gsigma = Evd.empty; genv = env })
     x
 
 (***************************************************************************)
@@ -913,11 +913,15 @@ let make_absolute_name ident repl =
 
 let add_tacdef local isrec tacl =
   let rfun = List.map (fun (ident, b, _) -> make_absolute_name ident b) tacl in
-  let ist =
-    { (make_empty_glob_sign ()) with ltacrecvars =
-	if isrec then List.map_filter
-	  (function (Some id, qid) -> Some (id, qid) | (None, _) -> None) rfun
-	else []} in
+  let ltacrecvars =
+    let fold accu (idopt, v) = match idopt with
+    | None -> accu
+    | Some id -> Id.Map.add id v accu
+    in
+    if isrec then List.fold_left fold Id.Map.empty rfun
+    else Id.Map.empty
+  in
+  let ist = { (make_empty_glob_sign ()) with ltacrecvars; } in
   let gtacl =
     List.map2 (fun (_,b,def) (id, qid) ->
       let k = if b then UpdateTac qid else NewTac (Option.get id) in
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index 53a04f7006..98d70ce108 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -25,7 +25,7 @@ open Nametab
 
 type glob_sign = Genintern.glob_sign = {
   ltacvars : Id.Set.t;
-  ltacrecvars : (Id.t * ltac_constant) list;
+  ltacrecvars : ltac_constant Id.Map.t;
   gsigma : Evd.evar_map;
   genv : Environ.env }
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 08b165b872..14c8c8f662 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1959,7 +1959,7 @@ let interp_tac_gen lfun avoid_ids debug t gl =
   let ltacvars = Id.Map.fold fold lfun Id.Set.empty in
   interp_tactic ist
     (intern_pure_tactic {
-      ltacvars; ltacrecvars = [];
+      ltacvars; ltacrecvars = Id.Map.empty;
       gsigma = project gl; genv = pf_env gl } t) gl
 
 let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
@@ -1970,7 +1970,7 @@ let eval_ltac_constr gl t =
 
 (* Used to hide interpretation for pretty-print, now just launch tactics *)
 let hide_interp t ot gl =
-  let ist = { ltacvars = Id.Set.empty; ltacrecvars = [];
+  let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
             gsigma = project gl; genv = pf_env gl } in
   let te = intern_pure_tactic ist t in
   let t = eval_tactic te in