From 53d23f52cd28c1373e784c278c8455cf9fa4eb67 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Sep 2003 14:41:39 +0000
Subject: Déplacement de Declare juste à la fin de interp pour pouvoir accéder
 à interp

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4365 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/classops.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'pretyping/classops.ml')

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index aa5057db8d..03a0da56ac 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -17,7 +17,6 @@ open Nametab
 open Environ
 open Libobject
 open Library
-open Declare
 open Term
 open Termops
 open Rawterm
@@ -240,11 +239,6 @@ let inductive_class_of ind = fst (class_info (CL_IND ind))
 
 let class_args_of c = snd (decompose_app c)
 
-let strength_of_cl = function 
-  | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn))
-  | CL_SECVAR sp -> variable_strength sp
-  | _ -> Global
-
 let string_of_class = function
   | CL_FUN -> if !Options.v7 then "FUNCLASS" else "Funclass"
   | CL_SORT -> if !Options.v7 then "SORTCLASS" else "Sortclass"
-- 
cgit v1.2.3