From 0256a92eb0d0265750bd38a85dce4f9487aefe5b Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 6 Oct 2012 10:08:51 +0000
Subject: still some more dead code removal

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof_global.ml | 9 ---------
 proofs/proof_type.ml   | 1 -
 2 files changed, 10 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 178c2ab2d8..25ed1f3e8b 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -125,15 +125,6 @@ let find_top l =
   | np::_ -> np
   | [] -> raise NoCurrentProof
 
-let rotate_top l1 l2 =
-  let np = extract_top l1 in
-  push np l2
-
-let rotate_find id l1 l2 =
-  let np = extract id l1 in
-  push np l2
-
-
 (* combinators for the proof_info map *)
 let add id info m =
   m := Idmap.add id info !m
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index e09d72e474..b7237f1fc4 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -12,7 +12,6 @@ open Names
 open Term
 open Tacexpr
 open Glob_term
-open Genarg
 open Nametab
 open Pattern
 open Misctypes
-- 
cgit v1.2.3