Replacing lists by maps in matching interpretation.

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

4 files changed, 10 insertions, 11 deletions

diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 979a7dae3..65971d6e3 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -62,12 +62,12 @@ let warn_bound_again name =
 
 let constrain n (ids, m as x) (names, terms as subst) =
   try
-    let (ids', m') = List.assoc n terms in
+    let (ids', m') = Id.Map.find n terms in
     if List.equal Id.equal ids ids' && eq_constr m m' then subst
     else raise PatternMatchingFailure
   with Not_found ->
     let () = if Id.Map.mem n names then warn_bound_meta n in
-    (names, (n, x) :: terms)
+    (names, Id.Map.add n x terms)
 
 let add_binders na1 na2 (names, terms as subst) = match na1, na2 with
 | Name id1, Name id2 ->
@@ -76,7 +76,7 @@ let add_binders na1 na2 (names, terms as subst) = match na1, na2 with
     (names, terms)
   else
     let names = Id.Map.add id1 id2 names in
-    let () = if List.mem_assoc id1 terms then warn_bound_again id1 in
+    let () = if Id.Map.mem id1 terms then warn_bound_again id1 in
     (names, terms)
 | _ -> subst
 
@@ -250,12 +250,11 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
       | _ -> raise PatternMatchingFailure
 
   in
-  let names, terms = sorec [] (Id.Map.empty, []) pat c in
-  (names, List.sort (fun (a, _) (b, _) -> Id.compare a b) terms)
+  sorec [] (Id.Map.empty, Id.Map.empty) pat c
 
 let matches_core_closed convert allow_partial_app pat c =
   let names, subst = matches_core convert allow_partial_app false pat c in
-  (names, List.map (fun (a,(_,b)) -> (a,b)) subst)
+  (names, Id.Map.map snd subst)
 
 let extended_matches = matches_core None true true
 
@@ -286,7 +285,7 @@ let matches_head pat c =
 let authorized_occ partial_app closed pat c mk_ctx next =
   try
     let sigma = matches_core_closed None partial_app pat c in
-    if closed && not (List.for_all (fun (_,c) -> closed0 c) (snd sigma))
+    if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd sigma)
     then Lazy.force next
     else mkresult sigma (mk_ctx (mkMeta special_meta)) next
   with PatternMatchingFailure -> Lazy.force next
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 5e4e5eb97..d695e8a45 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -203,7 +203,7 @@ let instantiate_pattern sigma lvar c =
   let rec aux vars = function
   | PVar id as x ->
       (try
-	let ctx,c = List.assoc id lvar in
+	let ctx,c = Id.Map.find id lvar in
 	try
 	  let inst =
 	    List.map (fun id -> mkRel (List.index (Name id) vars)) ctx in
@@ -213,7 +213,7 @@ let instantiate_pattern sigma lvar c =
 	  let vars =
 	    List.map_filter (function Name id -> Some id | _ -> None) vars in
 	  error_instantiate_pattern id (List.subtract ctx vars)
-       with Not_found (* List.assoc failed *) ->
+       with Not_found (* Map.find failed *) ->
 	 x)
   | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.")
   | c ->
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 4a4649cca..5cc4049ba 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -53,7 +53,7 @@ val pattern_of_glob_constr : glob_constr ->
       patvar list * constr_pattern
 
 val instantiate_pattern :
-  Evd.evar_map -> (Id.t * (Id.t list * constr)) list ->
+  Evd.evar_map -> extended_patvar_map ->
   constr_pattern -> constr_pattern
 
 val lift_pattern : int -> constr_pattern -> constr_pattern
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 31cf52eac..a8cdfd869 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -897,7 +897,7 @@ let contextually byhead (occs,c) f env sigma t =
 	else not (List.mem !pos locs) in
       incr pos;
       if ok then
-        let subst' = List.map (on_snd (traverse envc)) subst in
+        let subst' = Id.Map.map (traverse envc) subst in
 	f subst' env sigma t
       else if byhead then
 	(* find other occurrences of c in t; TODO: ensure left-to-right *)