Extraction: fix type_expunge_from_sign broken in last commit

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

1 files changed, 1 insertions, 25 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 69090bdd28..c11a8f1285 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -122,30 +122,6 @@ let rec nb_default_params env c =
 	if is_default env t then n+1 else n
     | _ -> 0
 
-(* Classification of signatures *)
-
-type sign_kind =
-  | EmptySig
-  | NonLogicalSig (* at least a [Keep] *)
-  | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *)
-  | SafeLogicalSig (* only [Kill Ktype] *)
-
-let rec sign_kind = function
-  | [] -> EmptySig
-  | Keep :: _ -> NonLogicalSig
-  | Kill k :: s ->
-      match sign_kind s with
-	| NonLogicalSig -> NonLogicalSig
-	| UnsafeLogicalSig -> UnsafeLogicalSig
-	| SafeLogicalSig | EmptySig ->
-	    if k = Kother then UnsafeLogicalSig else SafeLogicalSig
-
-(* Removing the final [Keep] in a signature *)
-
-let rec no_final_keeps = function
-  | [] -> []
-  | k :: s -> let s' = k :: no_final_keeps s in if s' = [Keep] then [] else s'
-
 (* Enriching a signature with implicit information *)
 
 let sign_with_implicits r s =
@@ -650,7 +626,7 @@ and extract_cst_app env mle mlt kn args =
   (* Now, the extraction of the arguments. *)
   let s_full = type2signature env (snd schema) in
   let s_full = sign_with_implicits (ConstRef kn) s_full in
-  let s = no_final_keeps s_full in
+  let s = sign_no_final_keeps s_full in
   let ls = List.length s in
   let la = List.length args in
   (* The ml arguments, already expunged from known logical ones *)