Suppression option immediate_discharge; nettoyage de Declare et conséquences

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

1 files changed, 0 insertions, 13 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 5a88e62dca..18bb390990 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -21,19 +21,6 @@ open Rawterm
 
 (* usage qque peu general: utilise aussi dans record *)
 
-type cte_typ = 
-  | NAM_Section_Variable of variable
-  | NAM_Constant of constant
-  | NAM_Inductive of inductive
-  | NAM_Constructor of constructor
-
-let cte_of_constr c = match kind_of_term c with
-  | IsConst sp -> ConstRef sp
-  | IsMutInd ind_sp -> IndRef ind_sp
-  | IsMutConstruct cstr_cp -> ConstructRef cstr_cp
-  | IsVar id -> VarRef (Declare.find_section_variable id)
-  |  _ -> raise Not_found
-
 type cl_typ = 
   | CL_SORT 
   | CL_FUN