6 files changed, 9 insertions, 21 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 41a068ff38..67c1c59017 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -19,7 +19,6 @@ open Table
 open Extraction
 open Modutil
 open Common
-open Mod_subst
 
 (***************************************)
 (*S Part I: computing Coq environment. *)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 667721e670..098f76bbfb 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -11,7 +11,6 @@ open Util
 open Names
 open Term
 open Vars
-open Context
 open Declarations
 open Declareops
 open Environ
@@ -26,6 +25,7 @@ open Globnames
 open Miniml
 open Table
 open Mlutil
+open Context.Rel.Declaration
 (*i*)
 
 exception I of inductive_kind
@@ -75,7 +75,7 @@ type flag = info * scheme
 let rec flag_of_type env t : flag =
   let t = whd_betadeltaiota env none t in
   match kind_of_term t with
-    | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c
+    | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c
     | Sort s when Sorts.is_prop s -> (Logic,TypeScheme)
     | Sort _ -> (Info,TypeScheme)
     | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default)
@@ -248,7 +248,7 @@ let rec extract_type env db j c args =
     | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kprop
     | Rel n ->
 	(match lookup_rel n env with
-           | (_,Some t,_) -> extract_type env db j (lift n t) args
+           | LocalDef (_,t,_) -> extract_type env db j (lift n t) args
 	   | _ ->
 	       (* Asks [db] a translation for [n]. *)
 	       if n > List.length db then Tunknown
@@ -561,7 +561,7 @@ let rec extract_term env mle mlt c args =
 	       put_magic_if magic (MLlam (id, d')))
     | LetIn (n, c1, t1, c2) ->
 	let id = id_of_name n in
-	let env' = push_rel (Name id, Some c1, t1) env in
+	let env' = push_rel (LocalDef (Name id, c1, t1)) env in
 	(* We directly push the args inside the [LetIn].
            TODO: the opt_let_app flag is supposed to prevent that *)
 	let args' = List.map (lift 1) args in
@@ -836,7 +836,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
 
 let decomp_lams_eta_n n m env c t =
   let rels = fst (splay_prod_n env none n t) in
-  let rels = List.map (fun (id,_,c) -> (id,c)) rels in
+  let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,c)) rels in
   let rels',c = decompose_lam c in
   let d = n - m in
   (* we'd better keep rels' as long as possible. *)
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index aec9586895..eb2f022443 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -11,6 +11,9 @@
 (* ML names *)
 
 open Genarg
+open Stdarg
+open Constrarg
+open Pcoq.Prim
 open Pp
 open Names
 open Nameops
@@ -31,7 +34,6 @@ let pr_int_or_id _ _ _ = function
   | ArgId id -> pr_id id
 
 ARGUMENT EXTEND int_or_id
-  TYPED AS int_or_id
   PRINTED BY pr_int_or_id
 | [ preident(id) ] -> [ ArgId (Id.of_string id) ]
 | [ integer(i) ] -> [ ArgInt i ]
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index df79c585e5..8874afef33 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -1,8 +1,6 @@
 open Pp
-open Errors
 open Util
 open Names
-open Nameops
 open Globnames
 open Table
 open Miniml
@@ -18,9 +16,6 @@ let json_int i =
 let json_bool b =
   if b then str "true" else str "false"
 
-let json_null =
-  str "null"
-
 let json_global typ ref =
   json_str (Common.pp_global typ ref)
 
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index b5e8b48044..bd48311308 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -380,14 +380,6 @@ let rec depcheck_struct = function
       let lse' = depcheck_se lse in
       if List.is_empty lse' then struc' else (mp,lse')::struc'
 
-let is_prefix pre s =
-  let len = String.length pre in
-  let rec is_prefix_aux i =
-    if Int.equal i len then true
-    else pre.[i] == s.[i] && is_prefix_aux (succ i)
-  in
-  is_prefix_aux 0
-
 exception RemainingImplicit of kill_reason
 
 let check_for_remaining_implicits struc =
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index d7842e127d..466c8054b8 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -453,7 +453,7 @@ let check_loaded_modfile mp = match base_mp mp with
       if not (Library.library_is_loaded dp) then begin
 	match base_mp (Lib.current_mp ()) with
 	  | MPfile dp' when not (DirPath.equal dp dp') ->
-	      err (str ("Please load library "^(DirPath.to_string dp^" first.")))
+	      err (str "Please load library " ++ pr_dirpath dp ++ str " first.")
 	  | _ -> ()
       end
   | _ -> ()