Generalizing the use of maps instead of lists in the interpretation

of tactics.

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

4 files changed, 12 insertions, 14 deletions

diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index e096ac4498..64f8e208eb 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -43,8 +43,7 @@ let instantiate n (ist,rawc) ido gl =
     let evk,_ = List.nth evl (n-1) in
     let evi = Evd.find sigma evk in
     let filtered = Evd.evar_filtered_env evi in
-    let (bvars, uvars) = Tacinterp.extract_ltac_constr_values ist filtered in
-    let ltac_vars = (Id.Map.bindings bvars, uvars) in
+    let ltac_vars = Tacinterp.extract_ltac_constr_values ist filtered in
     let sigma' = w_refine (evk,evi) (ltac_vars,rawc) sigma in
       tclTHEN
         (tclEVARS sigma')
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 3e008657fe..cfb96b488f 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -302,8 +302,9 @@ 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 c' =
-    warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars:(fst lfun,[]) sigma env) c
+    warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars sigma env) c
   in
   (c',if !strict_check then None else Some c)
 
@@ -440,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,[]) in
+      let ltacvars = (lfun, Id.Map.empty) in
       let (metas,pc) = intern_constr_pattern ist ltacvars pc in
       ido, metas, Subterm (b,ido,pc)
   | Term pc ->
-      let ltacvars = (lfun,[]) in
+      let ltacvars = (lfun, Id.Map.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 e0fe2cde41..852348e71e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -399,7 +399,7 @@ let interp_clause ist gl { onhyps=ol; concl_occs=occs } =
 
 (* Extract the constr list from lfun *)
 let extract_ltac_constr_values ist env =
-  let fold (id, v) (vars1, vars2) =
+  let fold (vars1, vars2) (id, v) =
     try
       let c = coerce_to_constr env v in
       (Id.Map.add id c vars1, vars2)
@@ -412,9 +412,9 @@ let extract_ltac_constr_values ist env =
           | _ -> None
         else None
       in
-      (vars1, (id, ido) :: vars2)
+      (vars1, Id.Map.add id ido vars2)
   in
-  List.fold_right fold ist.lfun (Id.Map.empty, [])
+  List.fold_left fold (Id.Map.empty, Id.Map.empty) ist.lfun
 
 (* Extract the identifier list from lfun: join all branches (what to do else?)*)
 let rec intropattern_ids (loc,pat) = match pat with
@@ -459,21 +459,20 @@ let pf_interp_fresh_id ist gl = interp_fresh_id ist (pf_env gl)
 
 let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   let (ltacvars,unbndltacvars as vars) = extract_ltac_constr_values ist env in
-  let ltacbnd = Id.Map.bindings ltacvars in
   let c = match ce with
   | None -> c
     (* If at toplevel (ce<>None), the error can be due to an incorrect
        context at globalization time: we retype with the now known
        intros/lettac/inversion hypothesis names *)
   | Some c ->
-      let ltacdata = (List.map fst ltacbnd, unbndltacvars) in
+      let fold id _ accu = id :: accu in
+      let ltacvars = Id.Map.fold fold ltacvars [] in
+      let ltacdata = (ltacvars, unbndltacvars) in
       intern_gen kind ~allow_patvar ~ltacvars:ltacdata sigma env c
   in
   let trace =
     push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in
   let (evd,c) =
-    (** FIXME: we should propagate the use of Id.Map.t everywhere *)
-    let vars = (ltacbnd, unbndltacvars) in
     catch_error trace (understand_ltac flags sigma env vars kind) c
   in
   db_constr (curr_debug ist) env c;
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 6affc21a47..32880fd771 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -45,8 +45,7 @@ val f_avoid_ids : Id.t list TacStore.field
 val f_debug : debug_info TacStore.field
 
 val extract_ltac_constr_values : interp_sign -> Environ.env ->
-  Pattern.constr_under_binders Id.Map.t * (Id.Map.key * Id.t option) list
-(* should be Pretyping.ltac_var_map *)
+  Pretyping.ltac_var_map
 
 (** Tactic extensions *)
 val add_tactic :