Extraction of Module with eq = ... : fix for bug #1853

(unrelated: a useless pattern variable becomes _ in Extract_env)



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

2 files changed, 12 insertions, 14 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index ef673dd4f..a1c3331c6 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -163,7 +163,7 @@ let rec extract_sfb_spec env mp = function
       let specs = extract_sfb_spec env mp msig in
       if logical_spec s then specs
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
-  | (l,SFBmind cb) :: msig ->
+  | (l,SFBmind _) :: msig ->
       let kn = make_kn mp empty_dirpath l in
       let s = Sind (kn, extract_inductive env kn) in
       let specs = extract_sfb_spec env mp msig in
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index b7be86bff..f9e2799a1 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -876,19 +876,17 @@ let extract_constant_spec env kn cb =
 	let t = snd (record_constant_type env kn (Some typ)) in 
 	Sval (r, type_expunge env t)
 
-let extract_with_type env cb = 
-  let typ = Typeops.type_of_constant_type env cb.const_type in 
-  match flag_of_type env typ with 
-    | (_ , Default) -> None
-    | (Logic, TypeScheme) ->Some ([],Tdummy Ktype)
-    | (Info, TypeScheme) -> 
-	let s,vl = type_sign_vl env typ in 
-	  (match cb.const_body with 
-	  | None -> assert false
-	  | Some body -> 
-	      let db = db_from_sign s in 
-	      let t = extract_type_scheme env db (force body) (List.length s)
-	      in Some ( vl, t) )
+let extract_with_type env cb =
+  let typ = Typeops.type_of_constant_type env cb.const_type in
+  match flag_of_type env typ with
+    | (Info, TypeScheme) ->
+	let s,vl = type_sign_vl env typ in
+	let body = Option.get cb.const_body in
+	let db = db_from_sign s in
+	let t = extract_type_scheme env db (force body) (List.length s) in
+	Some (vl, t)
+    | _ -> None
+
 		   
 let extract_inductive env kn = 
   let ind = extract_ind env kn in