Moved Intset and Intmap to Int namespace.

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

1 files changed, 35 insertions, 35 deletions

diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 20ec17269..5cb97d4bd 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -65,8 +65,8 @@ type form=
 module Fmap=Map.Make(struct type t=form let compare=compare end)
 
 type sequent =
-    {rev_hyps: form Intmap.t;
-     norev_hyps: form Intmap.t;
+    {rev_hyps: form Int.Map.t;
+     norev_hyps: form Int.Map.t;
      size:int;
      left:int Fmap.t;
      right:(int*form) list Fmap.t;
@@ -127,16 +127,16 @@ let add_step s sub =
 type 'a with_deps =
     {dep_it:'a;
      dep_goal:bool;
-     dep_hyps:Intset.t}
+     dep_hyps:Int.Set.t}
 
 type slice=
     {proofs_done:proof list;
      proofs_todo:sequent with_deps list;
      step:rule;
      needs_goal:bool;
-     needs_hyps:Intset.t;
+     needs_hyps:Int.Set.t;
      changes_goal:bool;
-     creates_hyps:Intset.t}
+     creates_hyps:Int.Set.t}
 
 type state =
     Complete of proof
@@ -161,25 +161,25 @@ let rec fill stack proof =
 	  !pruning &&
 	  slice.proofs_done=[] &&
 	  not (slice.changes_goal && proof.dep_goal) &&
-	  not (Intset.exists
-		 (fun i -> Intset.mem i proof.dep_hyps)
+	  not (Int.Set.exists
+		 (fun i -> Int.Set.mem i proof.dep_hyps)
 		 slice.creates_hyps)
 	then
 	  begin
 	    s_info.pruned_steps<-s_info.pruned_steps+1;
 	    s_info.pruned_branches<- s_info.pruned_branches +
 	    List.length slice.proofs_todo;
-	    let created_here=Intset.cardinal slice.creates_hyps in
+	    let created_here=Int.Set.cardinal slice.creates_hyps in
 	      s_info.pruned_hyps<-s_info.pruned_hyps+
 	      List.fold_left
-		(fun sum dseq -> sum + Intset.cardinal dseq.dep_hyps)
+		(fun sum dseq -> sum + Int.Set.cardinal dseq.dep_hyps)
 		created_here slice.proofs_todo;
-	    fill super (pop (Intset.cardinal slice.creates_hyps) proof)
+	    fill super (pop (Int.Set.cardinal slice.creates_hyps) proof)
 	  end
 	else
 	  let dep_hyps=
-	    Intset.union slice.needs_hyps
-	      (Intset.diff proof.dep_hyps slice.creates_hyps) in
+	    Int.Set.union slice.needs_hyps
+	      (Int.Set.diff proof.dep_hyps slice.creates_hyps) in
 	  let dep_goal=
 	    slice.needs_goal ||
 	    ((not slice.changes_goal) && proof.dep_goal) in
@@ -226,7 +226,7 @@ let append stack (step,subgoals) =
 let embed seq=
   {dep_it=seq;
    dep_goal=false;
-   dep_hyps=Intset.empty}
+   dep_hyps=Int.Set.empty}
 
 let change_goal seq gl=
     {seq with
@@ -261,7 +261,7 @@ let add_hyp seqwd f=
 	     cnx=cnx}
       | Conjunct (_,_) | Disjunct (_,_) ->
 	  {seq with
-	     rev_hyps=Intmap.add num f seq.rev_hyps;
+	     rev_hyps=Int.Map.add num f seq.rev_hyps;
 	     size=num;
 	     left=left;
 	     right=right;
@@ -276,14 +276,14 @@ let add_hyp seqwd f=
 	    match f1 with
 		Conjunct (_,_) | Disjunct (_,_) ->
 		  {seq with
-		     rev_hyps=Intmap.add num f seq.rev_hyps;
+		     rev_hyps=Int.Map.add num f seq.rev_hyps;
 		     size=num;
 		     left=left;
 		     right=nright;
 		     cnx=ncnx}
 	      | Arrow(_,_) ->
 		  {seq with
-		     norev_hyps=Intmap.add num f seq.norev_hyps;
+		     norev_hyps=Int.Map.add num f seq.norev_hyps;
 		     size=num;
 		     left=left;
 		     right=nright;
@@ -296,13 +296,13 @@ let add_hyp seqwd f=
 		     cnx=ncnx} in
     {seqwd with
        dep_it=nseq;
-       dep_hyps=Intset.add num seqwd.dep_hyps}
+       dep_hyps=Int.Set.add num seqwd.dep_hyps}
 
 exception Here_is of (int*form)
 
 let choose m=
   try
-    Intmap.iter (fun i f -> raise (Here_is (i,f))) m;
+    Int.Map.iter (fun i f -> raise (Here_is (i,f))) m;
     raise Not_found
   with
       Here_is (i,f) -> (i,f)
@@ -313,11 +313,11 @@ let search_or seq=
       Disjunct (f1,f2) ->
 	[{dep_it = SI_Or_l;
 	  dep_goal = true;
-	  dep_hyps = Intset.empty},
+	  dep_hyps = Int.Set.empty},
 	 [change_goal (embed seq) f1];
 	 {dep_it = SI_Or_r;
 	  dep_goal = true;
-	  dep_hyps = Intset.empty},
+	  dep_hyps = Int.Set.empty},
 	 [change_goal (embed seq) f2]]
     | _ -> []
 
@@ -327,11 +327,11 @@ let search_norev seq=
     match f with
 	Arrow (Arrow (f1,f2),f3) ->
 	  let nseq =
-	    {seq with norev_hyps=Intmap.remove i seq.norev_hyps} in
+	    {seq with norev_hyps=Int.Map.remove i seq.norev_hyps} in
 	    goals:=
 	      ({dep_it=SD_Arrow(i);
 		dep_goal=false;
-		dep_hyps=Intset.singleton i},
+		dep_hyps=Int.Set.singleton i},
 	       [add_hyp
 		  (add_hyp
 		     (change_goal (embed nseq) f2)
@@ -339,7 +339,7 @@ let search_norev seq=
 		  f1;
 		add_hyp (embed nseq) f3]):: !goals
       | _ -> anomaly "search_no_rev: can't happen" in
-    Intmap.iter add_one seq.norev_hyps;
+    Int.Map.iter add_one seq.norev_hyps;
     List.rev !goals
 
 let search_in_rev_hyps seq=
@@ -348,8 +348,8 @@ let search_in_rev_hyps seq=
     let make_step step=
       {dep_it=step;
        dep_goal=false;
-       dep_hyps=Intset.singleton i} in
-    let nseq={seq with rev_hyps=Intmap.remove i seq.rev_hyps} in
+       dep_hyps=Int.Set.singleton i} in
+    let nseq={seq with rev_hyps=Int.Map.remove i seq.rev_hyps} in
       match f with
 	  Conjunct (f1,f2) ->
 	    [make_step (SE_And(i)),
@@ -374,27 +374,27 @@ let search_rev seq=
 	  match f1 with
 	      Conjunct (_,_) | Disjunct (_,_) ->
 		{seq with cnx=next;
-		   rev_hyps=Intmap.remove j seq.rev_hyps}
+		   rev_hyps=Int.Map.remove j seq.rev_hyps}
 	    | Arrow (_,_) ->
 		{seq with cnx=next;
-		   norev_hyps=Intmap.remove j seq.norev_hyps}
+		   norev_hyps=Int.Map.remove j seq.norev_hyps}
 	    | _ ->
 		{seq with cnx=next} in
 	  [{dep_it=SE_Arrow(i,j);
 	    dep_goal=false;
-	    dep_hyps=Intset.add i (Intset.singleton j)},
+	    dep_hyps=Int.Set.add i (Int.Set.singleton j)},
 	   [add_hyp (embed nseq) f2]]
     | [] ->
 	match seq.gl with
 	    Arrow (f1,f2) ->
 	      [{dep_it=SI_Arrow;
 		dep_goal=true;
-		dep_hyps=Intset.empty},
+		dep_hyps=Int.Set.empty},
 	       [add_hyp (change_goal (embed seq) f2) f1]]
 	  | Conjunct (f1,f2) ->
 	      [{dep_it=SI_And;
 		dep_goal=true;
-		dep_hyps=Intset.empty},[change_goal (embed seq) f1;
+		dep_hyps=Int.Set.empty},[change_goal (embed seq) f1;
 					change_goal (embed seq) f2]]
 	  | _ -> search_in_rev_hyps seq
 
@@ -403,18 +403,18 @@ let search_all seq=
       Some i ->
 	[{dep_it=SE_False (i);
 	  dep_goal=false;
-	  dep_hyps=Intset.singleton i},[]]
+	  dep_hyps=Int.Set.singleton i},[]]
     | None ->
 	try
 	  let ax = Fmap.find seq.gl seq.left in
 	    [{dep_it=SAx (ax);
 	      dep_goal=true;
-	      dep_hyps=Intset.singleton ax},[]]
+	      dep_hyps=Int.Set.singleton ax},[]]
 	with Not_found -> search_rev seq
 
 let bare_sequent = embed
-		     {rev_hyps=Intmap.empty;
-		      norev_hyps=Intmap.empty;
+		     {rev_hyps=Int.Map.empty;
+		      norev_hyps=Int.Map.empty;
 		      size=0;
 		      left=Fmap.empty;
 		      right=Fmap.empty;
@@ -466,7 +466,7 @@ let pr_form f = pp_form f
 
 let pp_intmap map =
   let pp=ref (str "") in
-   Intmap.iter (fun i obj -> pp:= (!pp ++
+   Int.Map.iter (fun i obj -> pp:= (!pp ++
 		pp_form obj ++ cut ())) map;
     str "{ " ++ v 0 (!pp) ++ str " }"