Removing more association lists in Constrintern.

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

2 files changed, 16 insertions, 11 deletions

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 04c8c30644..52fb935d4e 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -278,7 +278,7 @@ let rec bind_primary_aliases map pat =
 	  List.fold_left bind_primary_aliases map1 lpat
 
 let bind_secondary_aliases map subst =
-  List.fold_left (fun map (ids,idp) -> (ids,List.assoc idp map)::map) map subst
+  Id.Map.fold (fun ids (idp : Id.t) map -> (ids,List.assoc idp map)::map) subst map
 
 let bind_aliases patvars subst patt =
   let map = bind_primary_aliases [] patt in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d1fa16c0a9..993f3d5fb0 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -491,11 +491,12 @@ let map_option f = function
 open Constrexpr
 open Topconstr
 
-let make_assoc = List.fold_left2 (fun l a b ->
-match a, b with
-  |(_,Name na), (_, Name id) -> (na, id)::l
-  |_,_ -> l
-)
+let make_assoc assoc l1 l2 =
+  let fold assoc a b = match a, b with
+  | (_, Name na), (_, Name id) -> Id.Map.add na id assoc
+  | _, _ -> assoc
+  in
+  List.fold_left2 fold assoc l1 l2
 
 let rec rebuild_bl (aux,assoc) bl typ = 
 	match bl,typ with 
@@ -514,16 +515,20 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	    let lnal' = List.length nal' in 
 	    if lnal' >= lnal 
 	    then 
-	      let old_nal',new_nal' = List.chop lnal nal' in 
-	      rebuild_bl ((LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't)::aux),(make_assoc assoc old_nal' nal)) bl' 
+	      let old_nal',new_nal' = List.chop lnal nal' in
+	      let nassoc = make_assoc assoc old_nal' nal in
+	      let assum = LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't) in
+	      rebuild_bl ((assum :: aux), nassoc) bl' 
 		(if new_nal' = [] && rest = []
 		 then  typ' 
 		 else if new_nal' = [] 
 		 then CProdN(Loc.ghost,rest,typ')
 		 else CProdN(Loc.ghost,((new_nal',bk',nal't)::rest),typ'))
 	    else 
-	      let captured_nal,non_captured_nal = List.chop lnal' nal in 
-	      rebuild_nal ((LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't)::aux), (make_assoc assoc nal' captured_nal))
+	      let captured_nal,non_captured_nal = List.chop lnal' nal in
+	      let nassoc = make_assoc assoc nal' captured_nal in
+	      let assum = LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in
+	      rebuild_nal ((assum :: aux), nassoc)
 		bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ'))
 	  | _ -> assert false
 
@@ -537,7 +542,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
   let fixpoint_exprl_with_new_bl = 
     List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> 
      
-      let new_bl',new_ret_type,_ = rebuild_bl ([],[]) bl fix_typ in 
+      let new_bl',new_ret_type,_ = rebuild_bl ([],Id.Map.empty) bl fix_typ in 
       (((lna,(rec_arg_opt,rec_order),new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
     )
       fixpoint_exprl constr_expr_typel