Imported Upstream version 8.5~beta1+dfsg

1 files changed, 186 insertions, 140 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index a5b1e3c6..080512b2 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,7 +10,10 @@
 open Util
 open Names
 open Term
+open Vars
+open Context
 open Declarations
+open Declareops
 open Environ
 open Reduction
 open Reductionops
@@ -19,9 +22,7 @@ open Termops
 open Inductiveops
 open Recordops
 open Namegen
-open Summary
-open Libnames
-open Nametab
+open Globnames
 open Miniml
 open Table
 open Mlutil
@@ -36,13 +37,13 @@ let none = Evd.empty
 
 let type_of env c =
   try
-    let polyprop = (lang() = Haskell) in
+    let polyprop = (lang() == Haskell) in
     Retyping.get_type_of ~polyprop env none (strip_outer_cast c)
   with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
 
 let sort_of env c =
   try
-    let polyprop = (lang() = Haskell) in
+    let polyprop = (lang() == Haskell) in
     Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c)
   with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
 
@@ -55,8 +56,8 @@ let sort_of env c =
      More formally, a type scheme has type $(x_1:X_1)\ldots(x_n:X_n)s$ with
      [s = Set], [Prop] or [Type]
    \item [Default] denotes the other cases. It may be inexact after
-     instanciation. For example [(X:Type)X] is [Default] and may give [Set]
-     after instanciation, which is rather [TypeScheme]
+     instantiation. For example [(X:Type)X] is [Default] and may give [Set]
+     after instantiation, which is rather [TypeScheme]
    \item [Logic] denotes a term of sort [Prop], or a type scheme on sort [Prop]
    \item [Info] is the opposite. The same example [(X:Type)X] shows
      that an [Info] term might in fact be [Logic] later on.
@@ -71,17 +72,19 @@ type flag = info * scheme
 (*s [flag_of_type] transforms a type [t] into a [flag].
   Really important function. *)
 
-let rec flag_of_type env t =
+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
-    | Sort (Prop Null) -> (Logic,TypeScheme)
+    | Sort s when Sorts.is_prop s -> (Logic,TypeScheme)
     | Sort _ -> (Info,TypeScheme)
-    | _ -> if (sort_of env t) = InProp then (Logic,Default) else (Info,Default)
+    | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default)
 
 (*s Two particular cases of [flag_of_type]. *)
 
-let is_default env t = (flag_of_type env t = (Info, Default))
+let is_default env t = match flag_of_type env t with
+| (Info, Default) -> true
+| _ -> false
 
 exception NotDefault of kill_reason
 
@@ -91,7 +94,9 @@ let check_default env t =
     | Logic,_ -> raise (NotDefault Kother)
     | _ -> ()
 
-let is_info_scheme env t = (flag_of_type env t = (Info, TypeScheme))
+let is_info_scheme env t = match flag_of_type env t with
+| (Info, TypeScheme) -> true
+| _ -> false
 
 (*s [type_sign] gernerates a signature aimed at treating a type application. *)
 
@@ -109,16 +114,31 @@ let rec type_scheme_nb_args env c =
 	if is_info_scheme env t then n+1 else n
     | _ -> 0
 
-let _ = register_type_scheme_nb_args type_scheme_nb_args
+let _ = Hook.set type_scheme_nb_args_hook type_scheme_nb_args
 
 (*s [type_sign_vl] does the same, plus a type var list. *)
 
+(* When generating type variables, we avoid any ' in their names
+   (otherwise this may cause a lexer conflict in ocaml with 'a').
+   We also get rid of unicode characters. Anyway, since type variables
+   are local, the created name is just a matter of taste...
+   See also Bug #3227 *)
+
+let make_typvar n vl =
+  let id = id_of_name n in
+  let id' =
+    let s = Id.to_string id in
+    if not (String.contains s '\'') && Unicode.is_basic_ascii s then id
+    else id_of_name Anonymous
+  in
+  next_ident_away id' vl
+
 let rec type_sign_vl env c =
   match kind_of_term (whd_betadeltaiota env none c) with
     | Prod (n,t,d) ->
 	let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in
 	if not (is_info_scheme env t) then Kill Kother::s, vl
-	else Keep::s, (next_ident_away (id_of_name n) vl) :: vl
+	else Keep::s, (make_typvar n vl) :: vl
     | _ -> [],[]
 
 let rec nb_default_params env c =
@@ -136,7 +156,8 @@ let sign_with_implicits r s nb_params =
     | [] -> []
     | sign::s ->
 	let sign' =
-	  if sign = Keep && List.mem i implicits then Kill Kother else sign
+	  if sign == Keep && Int.List.mem i implicits
+          then Kill Kother else sign
 	in sign' :: add_impl (succ i) s
   in
   add_impl (1+nb_params) s
@@ -145,11 +166,11 @@ let sign_with_implicits r s nb_params =
 
 let rec handle_exn r n fn_name = function
   | MLexn s ->
-      (try Scanf.sscanf s "UNBOUND %d"
+      (try Scanf.sscanf s "UNBOUND %d%!"
 	 (fun i ->
 	    assert ((0 < i) && (i <= n));
 	    MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i)))
-       with e when Errors.noncritical e -> MLexn s)
+       with Scanf.Scan_failure _ | End_of_file -> MLexn s)
   | a -> ast_map (handle_exn r n fn_name) a
 
 (*S Management of type variable contexts. *)
@@ -170,8 +191,8 @@ let db_from_sign s =
   an inductive type (see just below). *)
 
 let rec db_from_ind dbmap i =
-  if i = 0 then []
-  else (try Intmap.find i dbmap with Not_found -> 0)::(db_from_ind dbmap (i-1))
+  if Int.equal i 0 then []
+  else (try Int.Map.find i dbmap with Not_found -> 0)::(db_from_ind dbmap (i-1))
 
 (*s [parse_ind_args] builds a map: [i->j] iff the i-th Coq argument
   of a constructor corresponds to the j-th type var of the ML inductive. *)
@@ -185,34 +206,43 @@ let rec db_from_ind dbmap i =
 
 let parse_ind_args si args relmax =
   let rec parse i j = function
-    | [] -> Intmap.empty
+    | [] -> Int.Map.empty
     | Kill _ :: s -> parse (i+1) j s
     | Keep :: s ->
       (match kind_of_term args.(i-1) with
-	 | Rel k -> Intmap.add (relmax+1-k) j (parse (i+1) (j+1) s)
+	 | Rel k -> Int.Map.add (relmax+1-k) j (parse (i+1) (j+1) s)
 	 | _ -> parse (i+1) (j+1) s)
   in parse 1 1 si
 
 let oib_equal o1 o2 =
-  id_ord o1.mind_typename o2.mind_typename = 0 &&
-  list_equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
-  begin match o1.mind_arity, o2.mind_arity with
-  | Monomorphic {mind_user_arity=c1; mind_sort=s1},
-    Monomorphic {mind_user_arity=c2; mind_sort=s2} ->
-      eq_constr c1 c2 && s1 = s2
-  | ma1, ma2 -> ma1 = ma2 end &&
-  o1.mind_consnames = o2.mind_consnames
+  Id.equal o1.mind_typename o2.mind_typename &&
+  List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
+    begin
+      match o1.mind_arity, o2.mind_arity with
+      | RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} ->
+	eq_constr c1 c2 && Sorts.equal s1 s2
+      | TemplateArity p1, TemplateArity p2 ->
+	let eq o1 o2 = Option.equal Univ.Level.equal o1 o2 in
+	  List.equal eq p1.template_param_levels p2.template_param_levels &&
+	    Univ.Universe.equal p1.template_level p2.template_level
+      | _, _ -> false
+    end &&
+    Array.equal Id.equal o1.mind_consnames o2.mind_consnames
+
+let eq_record x y =
+  Option.equal (Option.equal (fun (_, x, y) (_, x', y') -> Array.for_all2 eq_constant x x')) x y
 
 let mib_equal m1 m2 =
-  array_equal oib_equal m1.mind_packets m1.mind_packets &&
-  m1.mind_record = m2.mind_record &&
-  m1.mind_finite = m2.mind_finite &&
-  m1.mind_ntypes = m2.mind_ntypes &&
-  list_equal eq_named_declaration m1.mind_hyps m2.mind_hyps &&
-  m1.mind_nparams = m2.mind_nparams &&
-  m1.mind_nparams_rec = m2.mind_nparams_rec &&
-  list_equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt &&
-  m1.mind_constraints = m2.mind_constraints
+  Array.equal oib_equal m1.mind_packets m1.mind_packets &&
+  eq_record m1.mind_record m2.mind_record &&
+  (m1.mind_finite : Decl_kinds.recursivity_kind) == m2.mind_finite &&
+  Int.equal m1.mind_ntypes m2.mind_ntypes &&
+  List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps &&
+  Int.equal m1.mind_nparams m2.mind_nparams &&
+  Int.equal m1.mind_nparams_rec m2.mind_nparams_rec &&
+  List.equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt &&
+  (* Univ.UContext.eq *) m1.mind_universes == m2.mind_universes (** FIXME *)
+  (* m1.mind_universes = m2.mind_universes *)
 
 (*S Extraction of a type. *)
 
@@ -235,7 +265,7 @@ let rec extract_type env db j c args =
 	   | [] -> assert false (* A lambda cannot be a type. *)
 	   | a :: args -> extract_type env db j (subst1 a d) args)
     | Prod (n,t,d) ->
-	assert (args = []);
+	assert (List.is_empty args);
 	let env' = push_rel_assum (n,t) env in
 	(match flag_of_type env t with
 	   | (Info, Default) ->
@@ -255,10 +285,10 @@ let rec extract_type env db j c args =
 	       (match expand env mld with
 		  | Tdummy d -> Tdummy d
 		  | _ ->
-		      let reason = if lvl=TypeScheme then Ktype else Kother in
+		      let reason = if lvl == TypeScheme then Ktype else Kother in
 		      Tarr (Tdummy reason, mld)))
     | Sort _ -> Tdummy Ktype (* The two logical cases. *)
-    | _ when sort_of env (applist (c, args)) = InProp -> Tdummy Kother
+    | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kother
     | Rel n ->
 	(match lookup_rel n env with
            | (_,Some t,_) -> extract_type env db j (lift n t) args
@@ -266,11 +296,11 @@ let rec extract_type env db j c args =
 	       (* Asks [db] a translation for [n]. *)
 	       if n > List.length db then Tunknown
 	       else let n' = List.nth db (n-1) in
-	       if n' = 0 then Tunknown else Tvar n')
-    | Const kn ->
+	       if Int.equal n' 0 then Tunknown else Tvar n')
+    | Const (kn,u as c) ->
 	let r = ConstRef kn in
 	let cb = lookup_constant kn env in
-	let typ = Typeops.type_of_constant_type env cb.const_type in
+	let typ,_ = Typeops.type_of_constant env c in
 	(match flag_of_type env typ with
 	   | (Logic,_) -> assert false (* Cf. logical cases above *)
 	   | (Info, TypeScheme) ->
@@ -279,23 +309,23 @@ let rec extract_type env db j c args =
 		  | Undef _ | OpaqueDef _ -> mlt
 		  | Def _ when is_custom r -> mlt
 		  | Def lbody ->
-		      let newc = applist (Declarations.force lbody, args) in
+		      let newc = applist (Mod_subst.force_constr lbody, args) in
 		      let mlt' = extract_type env db j newc [] in
 		      (* ML type abbreviations interact badly with Coq *)
 		      (* reduction, so [mlt] and [mlt'] might be different: *)
 		      (* The more precise is [mlt'], extracted after reduction *)
 		      (* The shortest is [mlt], which use abbreviations *)
 		      (* If possible, we take [mlt], otherwise [mlt']. *)
-		      if expand env mlt = expand env mlt' then mlt else mlt')
+		      if eq_ml_type (expand env mlt) (expand env mlt') then mlt else mlt')
 	   | (Info, Default) ->
                (* Not an ML type, for example [(c:forall X, X->X) Type nat] *)
 	       (match cb.const_body with
 		  | Undef _  | OpaqueDef _ -> Tunknown (* Brutal approx ... *)
 		  | Def lbody ->
 		      (* We try to reduce. *)
-		      let newc = applist (Declarations.force lbody, args) in
+		      let newc = applist (Mod_subst.force_constr lbody, args) in
 		      extract_type env db j newc []))
-    | Ind (kn,i) ->
+    | Ind ((kn,i),u) ->
 	let s = (extract_ind env kn).ind_packets.(i).ip_sign in
 	extract_type_app env db (IndRef (kn,i),s) args
     | Case _ | Fix _ | CoFix _ -> Tunknown
@@ -308,7 +338,7 @@ let rec extract_type env db j c args =
 and extract_type_app env db (r,s) args =
   let ml_args =
     List.fold_right
-      (fun (b,c) a -> if b=Keep then
+      (fun (b,c) a -> if b == Keep then
 	 let p = List.length (fst (splay_prod env none (type_of env c))) in
          let db = iterate (fun l -> 0 :: l) p db in
          (extract_type_scheme env db c p) :: a
@@ -326,7 +356,7 @@ and extract_type_app env db (r,s) args =
 (* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
 
 and extract_type_scheme env db c p =
-  if p=0 then extract_type env db 0 c []
+  if Int.equal p 0 then extract_type env db 0 c []
   else
     let c = whd_betaiotazeta Evd.empty c in
     match kind_of_term c with
@@ -335,7 +365,7 @@ and extract_type_scheme env db c p =
       | _ ->
           let rels = fst (splay_prod env none (type_of env c)) in
           let env = push_rels_assum rels env in
-          let eta_args = List.rev_map mkRel (interval 1 p) in
+          let eta_args = List.rev_map mkRel (List.interval 1 p) in
           extract_type env db 0 (lift p c) eta_args
 
 
@@ -356,9 +386,9 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
        When at toplevel of the monolithic case, we cannot do much
        (cf Vector and bug #2570) *)
     let equiv =
-      if lang () <> Ocaml ||
+      if lang () != Ocaml ||
 	 (not (modular ()) && at_toplevel (mind_modpath kn)) ||
-	 kn_ord (canonical_mind kn) (user_mind kn) = 0
+	 KerName.equal (canonical_mind kn) (user_mind kn)
       then
 	NoEquiv
       else
@@ -375,32 +405,34 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     (* First pass: we store inductive signatures together with *)
     (* their type var list. *)
     let packets =
-      Array.map
-	(fun mip ->
-	   let b = snd (mind_arity mip) <> InProp in
-	   let ar = Inductive.type_of_inductive env (mib,mip) in
-	   let s,v = if b then type_sign_vl env ar else [],[] in
+      Array.mapi
+	(fun i mip ->
+	   let (ind,u), ctx = 
+	     Universes.fresh_inductive_instance env (kn,i) in
+	   let ar = Inductive.type_of_inductive env ((mib,mip),u) in
+	   let info = (fst (flag_of_type env ar) = Info) in
+	   let s,v = if info then type_sign_vl env ar else [],[] in
 	   let t = Array.make (Array.length mip.mind_nf_lc) [] in
 	   { ip_typename = mip.mind_typename;
 	     ip_consnames = mip.mind_consnames;
-	     ip_logical = (not b);
+	     ip_logical = not info;
 	     ip_sign = s;
 	     ip_vars = v;
-	     ip_types = t })
+	     ip_types = t }, u)
 	mib.mind_packets
     in
 
     add_ind kn mib
       {ind_kind = Standard;
        ind_nparams = npar;
-       ind_packets = packets;
+       ind_packets = Array.map fst packets;
        ind_equiv = equiv
       };
     (* Second pass: we extract constructors *)
     for i = 0 to mib.mind_ntypes - 1 do
-      let p = packets.(i) in
+      let p,u = packets.(i) in
       if not p.ip_logical then
-	let types = arities_of_constructors env (kn,i) in
+	let types = arities_of_constructors env ((kn,i),u) in
 	for j = 0 to Array.length types - 1 do
 	  let t = snd (decompose_prod_n npar types.(j)) in
 	  let prods,head = dest_prod epar t in
@@ -420,18 +452,18 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	let ip = (kn, 0) in
 	let r = IndRef ip in
 	if is_custom r then raise (I Standard);
-	if not mib.mind_finite then raise (I Coinductive);
-	if mib.mind_ntypes <> 1 then raise (I Standard);
-	let p = packets.(0) in
+	if mib.mind_finite == Decl_kinds.CoFinite then raise (I Coinductive);
+	if not (Int.equal mib.mind_ntypes 1) then raise (I Standard);
+	let p,u = packets.(0) in
 	if p.ip_logical then raise (I Standard);
-	if Array.length p.ip_types <> 1 then raise (I Standard);
+	if not (Int.equal (Array.length p.ip_types) 1) then raise (I Standard);
 	let typ = p.ip_types.(0) in
 	let l = List.filter (fun t -> not (isDummy (expand env t))) typ in
 	if not (keep_singleton ()) &&
-	    List.length l = 1 && not (type_mem_kn kn (List.hd l))
+	    Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l))
 	then raise (I Singleton);
-	if l = [] then raise (I Standard);
-	if not mib.mind_record then raise (I Standard);
+	if List.is_empty l then raise (I Standard);
+	if Option.is_empty mib.mind_record then raise (I Standard);
 	(* Now we're sure it's a record. *)
 	(* First, we find its field names. *)
 	let rec names_prod t = match kind_of_term t with
@@ -441,10 +473,10 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  | _ -> []
 	in
 	let field_names =
-	  list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
-	assert (List.length field_names = List.length typ);
+	  List.skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
+	assert (Int.equal (List.length field_names) (List.length typ));
 	let projs = ref Cset.empty in
-	let mp,d,_ = repr_mind kn in
+	let mp = MutInd.modpath kn in
 	let rec select_fields l typs = match l,typs with
 	  | [],[] -> []
 	  | _::l, typ::typs when isDummy (expand env typ) ->
@@ -452,9 +484,9 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  | Anonymous::l, typ::typs ->
 	      None :: (select_fields l typs)
 	  | Name id::l, typ::typs ->
-	      let knp = make_con mp d (label_of_id id) in
+	      let knp = Constant.make2 mp (Label.of_id id) in
 	      (* Is it safe to use [id] for projections [foo.id] ? *)
-	      if List.for_all ((=) Keep) (type2signature env typ)
+	      if List.for_all ((==) Keep) (type2signature env typ)
 	      then projs := Cset.add knp !projs;
 	      Some (ConstRef knp) :: (select_fields l typs)
 	  | _ -> assert false
@@ -465,9 +497,10 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	(* If so, we use this information. *)
 	begin try
 	  let n = nb_default_params env
-            (Inductive.type_of_inductive env (mib,mip0))
+            (Inductive.type_of_inductive env ((mib,mip0),u))
 	  in
-	  let check_proj kn = if Cset.mem kn !projs then add_projection n kn in
+	  let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip
+          in
 	  List.iter (Option.iter check_proj) (lookup_projections ip)
 	with Not_found -> ()
 	end;
@@ -476,7 +509,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     in
     let i = {ind_kind = ind_info;
 	     ind_nparams = npar;
-	     ind_packets = packets;
+	     ind_packets = Array.map fst packets;
 	     ind_equiv = equiv }
     in
     add_ind kn mib i;
@@ -495,7 +528,7 @@ and extract_type_cons env db dbmap c i =
   match kind_of_term (whd_betadeltaiota env none c) with
     | Prod (n,t,d) ->
 	let env' = push_rel_assum (n,t) env in
-	let db' = (try Intmap.find i dbmap with Not_found -> 0) :: db in
+	let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in
 	let l = extract_type_cons env' db' dbmap d (i+1) in
 	(extract_type env db 0 t []) :: l
     | _ -> []
@@ -511,13 +544,14 @@ and mlt_env env r = match r with
 	   | _ -> None
        with Not_found ->
 	 let cb = Environ.lookup_constant kn env in
-	 let typ = Typeops.type_of_constant_type env cb.const_type in
+	 let typ = Typeops.type_of_constant_type env cb.const_type
+ (* FIXME not sure if we should instantiate univs here *) in
 	 match cb.const_body with
 	   | Undef _ | OpaqueDef _ -> None
 	   | Def l_body ->
 	       (match flag_of_type env typ with
 		  | Info,TypeScheme ->
-		      let body = Declarations.force l_body in
+		      let body = Mod_subst.force_constr l_body in
 		      let s,vl = type_sign_vl env typ in
 		      let db = db_from_sign s in
 		      let t = extract_type_scheme env db body (List.length s)
@@ -539,7 +573,7 @@ let record_constant_type env kn opt_typ =
     lookup_type kn
   with Not_found ->
     let typ = match opt_typ with
-      | None -> Typeops.type_of_constant env kn
+      | None -> Typeops.type_of_constant_type env (lookup_constant kn env).const_type
       | Some typ -> typ
     in let mlt = extract_type env [] 1 typ []
     in let schema = (type_maxvar mlt, mlt)
@@ -594,10 +628,12 @@ let rec extract_term env mle mlt c args =
 	with NotDefault d ->
 	  let mle' = Mlenv.push_std_type mle (Tdummy d) in
 	  ast_pop (extract_term env' mle' mlt c2 args'))
-    | Const kn ->
-	extract_cst_app env mle mlt kn args
-    | Construct cp ->
-	extract_cons_app env mle mlt cp args
+    | Const (kn,u) ->
+	extract_cst_app env mle mlt kn u args
+    | Construct (cp,u) ->
+	extract_cons_app env mle mlt cp u args
+    | Proj (p, c) ->
+        extract_cst_app env mle mlt (Projection.constant p) Univ.Instance.empty (c :: args)
     | Rel n ->
 	(* As soon as the expected [mlt] for the head is known, *)
 	(* we unify it with an fresh copy of the stored type of [Rel n]. *)
@@ -645,14 +681,15 @@ and make_mlargs env e s args typs =
 
 (*s Extraction of a constant applied to arguments. *)
 
-and extract_cst_app env mle mlt kn args =
+and extract_cst_app env mle mlt kn u args =
   (* First, the [ml_schema] of the constant, in expanded version. *)
   let nb,t = record_constant_type env kn None in
   let schema = nb, expand env t in
   (* Can we instantiate types variables for this constant ? *)
   (* In Ocaml, inside the definition of this constant, the answer is no. *)
   let instantiated =
-    if lang () = Ocaml && List.mem kn !current_fixpoints then var2var' (snd schema)
+    if lang () == Ocaml && List.mem_f Constant.equal kn !current_fixpoints
+    then var2var' (snd schema)
     else instantiation schema
   in
   (* Then the expected type of this constant. *)
@@ -674,14 +711,14 @@ and extract_cst_app env mle mlt kn args =
   (* The ml arguments, already expunged from known logical ones *)
   let mla = make_mlargs env mle s args metas in
   let mla =
-    if magic1 || lang () <> Ocaml then mla
+    if magic1 || lang () != Ocaml then mla
     else
       try
         (* for better optimisations later, we discard dependent args
            of projections and replace them by fake args that will be
            removed during final pretty-print. *)
-	let l,l' = list_chop (projection_arity (ConstRef kn)) mla in
-	if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
+	let l,l' = List.chop (projection_arity (ConstRef kn)) mla in
+	if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
 	else mla
       with e when Errors.noncritical e -> mla
   in
@@ -689,7 +726,7 @@ and extract_cst_app env mle mlt kn args =
      one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
      accordingly. *)
   let optdummy = match sign_kind s_full with
-    | UnsafeLogicalSig when lang () <> Haskell -> [MLdummy]
+    | UnsafeLogicalSig when lang () != Haskell -> [MLdummy]
     | _ -> []
   in
   (* Different situations depending of the number of arguments: *)
@@ -702,7 +739,7 @@ and extract_cst_app env mle mlt kn args =
     (* Partially applied function with some logical arg missing.
        We complete via eta and expunge logical args. *)
     let ls' = ls-la in
-    let s' = list_skipn la s in
+    let s' = List.skipn la s in
     let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
     let e = anonym_or_dummy_lams (mlapp head mla) s' in
     put_magic_if magic2 (remove_n_lams (List.length optdummy) e)
@@ -717,14 +754,14 @@ and extract_cst_app env mle mlt kn args =
    they are fixed, and thus are not used for the computation.
    \end{itemize} *)
 
-and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
+and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args =
   (* First, we build the type of the constructor, stored in small pieces. *)
   let mi = extract_ind env kn in
   let params_nb = mi.ind_nparams in
   let oi = mi.ind_packets.(i) in
   let nb_tvars = List.length oi.ip_vars
   and types = List.map (expand env) oi.ip_types.(j-1) in
-  let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in
+  let list_tvar = List.map (fun i -> Tvar i) (List.interval 1 nb_tvars) in
   let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
   let type_cons = instantiation (nb_tvars, type_cons) in
   (* Then, the usual variables [s], [ls], [la], ... *)
@@ -734,7 +771,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let la = List.length args in
   assert (la <= ls + params_nb);
   let la' = max 0 (la - params_nb) in
-  let args' = list_lastn la' args in
+  let args' = List.lastn la' args in
   (* Now, we build the expected type of the constructor *)
   let metas = List.map new_meta args' in
   (* If stored and expected types differ, then magic! *)
@@ -742,7 +779,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in
   let magic2 = needs_magic (a, mlt) in
   let head mla =
-    if mi.ind_kind = Singleton then
+    if mi.ind_kind == Singleton then
       put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *)
     else
       let typeargs = match snd (type_decomp type_cons) with
@@ -759,11 +796,11 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
       (dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la))
   else
     let mla = make_mlargs env mle s args' metas in
-    if la = ls + params_nb
+    if Int.equal la (ls + params_nb)
     then put_magic_if (magic2 && not magic1) (head mla)
     else (* [ params_nb <= la <= ls + params_nb ] *)
       let ls' = params_nb + ls - la in
-      let s' = list_lastn ls' s in
+      let s' = List.lastn ls' s in
       let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
       put_magic_if magic2 (anonym_or_dummy_lams (head mla) s')
 
@@ -772,22 +809,22 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
 and extract_case env mle ((kn,i) as ip,c,br) mlt =
   (* [br]: bodies of each branch (in functional form) *)
   (* [ni]: number of arguments without parameters in each branch *)
-  let ni = mis_constr_nargs_env env ip in
+  let ni = constructors_nrealargs_env env ip in
   let br_size = Array.length br in
-  assert (Array.length ni = br_size);
-  if br_size = 0 then begin
+  assert (Int.equal (Array.length ni) br_size);
+  if Int.equal br_size 0 then begin
     add_recursors env kn; (* May have passed unseen if logical ... *)
     MLexn "absurd case"
   end else
     (* [c] has an inductive type, and is not a type scheme type. *)
     let t = type_of env c in
     (* The only non-informative case: [c] is of sort [Prop] *)
-    if (sort_of env t) = InProp then
+    if (sort_of env t) == InProp then
       begin
 	add_recursors env kn; (* May have passed unseen if logical ... *)
 	(* Logical singleton case: *)
 	(* [match c with C i j k -> t] becomes [t'] *)
-	assert (br_size = 1);
+	assert (Int.equal br_size 1);
 	let s = iterate (fun l -> Kill Kother :: l) ni.(0) [] in
 	let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni.(0) mlt in
 	let e = extract_maybe_term env mle mlt br.(0) in
@@ -816,13 +853,13 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in
 	(List.rev ids, Pusual r, e')
       in
-      if mi.ind_kind = Singleton then
+      if mi.ind_kind == Singleton then
 	begin
 	  (* Informative singleton case: *)
 	  (* [match c with C i -> t] becomes [let i = c' in t'] *)
-	  assert (br_size = 1);
+	  assert (Int.equal br_size 1);
 	  let (ids,_,e') = extract_branch 0 in
-	  assert (List.length ids = 1);
+	  assert (Int.equal (List.length ids) 1);
 	  MLletin (tmp_id (List.hd ids),a,e')
 	end
       else
@@ -838,7 +875,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
   let metas = Array.map new_meta fi in
   metas.(i) <- mlt;
   let mle = Array.fold_left Mlenv.push_type mle metas in
-  let ei = array_map2 (extract_maybe_term env mle) metas ci in
+  let ei = Array.map2 (extract_maybe_term env mle) metas ci in
   MLfix (i, Array.map id_of_name fi, ei)
 
 (*S ML declarations. *)
@@ -846,14 +883,14 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
 (* [decomp_lams_eta env c t] finds the number [n] of products in the type [t],
    and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *)
 
-let rec decomp_lams_eta_n n m env c t =
+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',c = decompose_lam c in
   let d = n - m in
   (* we'd better keep rels' as long as possible. *)
-  let rels = (list_firstn d rels) @ rels' in
-  let eta_args = List.rev_map mkRel (interval 1 d) in
+  let rels = (List.firstn d rels) @ rels' in
+  let eta_args = List.rev_map mkRel (List.interval 1 d) in
   rels, applist (lift d c,eta_args)
 
 (* Let's try to identify some situation where extracted code
@@ -864,7 +901,7 @@ let rec gentypvar_ok c = match kind_of_term c with
   | App (c,v) ->
       (* if all arguments are variables, these variables will
 	 disappear after extraction (see [empty_s] below) *)
-      array_for_all isRel v && gentypvar_ok c
+      Array.for_all isRel v && gentypvar_ok c
   | Cast (c,_,_) -> gentypvar_ok c
   | _ -> false
 
@@ -891,26 +928,26 @@ let extract_std_constant env kn body typ =
     and m = nb_lam body in
     if n <= m then decompose_lam_n n body
     else
-      let s,s' = list_chop m s in
-      if List.for_all ((=) Keep) s' &&
-	(lang () = Haskell || sign_kind s <> UnsafeLogicalSig)
+      let s,s' = List.chop m s in
+      if List.for_all ((==) Keep) s' &&
+	(lang () == Haskell || sign_kind s != UnsafeLogicalSig)
       then decompose_lam_n m body
       else decomp_lams_eta_n n m env body typ
   in
   (* Should we do one eta-expansion to avoid non-generalizable '_a ? *)
   let rels, c =
     let n = List.length rels in
-    let s,s' = list_chop n s in
+    let s,s' = List.chop n s in
     let k = sign_kind s in
-    let empty_s = (k = EmptySig || k = SafeLogicalSig) in
-    if lang () = Ocaml && empty_s && not (gentypvar_ok c)
-      && s' <> [] && type_maxvar t <> 0
+    let empty_s = (k == EmptySig || k == SafeLogicalSig) in
+    if lang () == Ocaml && empty_s && not (gentypvar_ok c)
+      && not (List.is_empty s') && not (Int.equal (type_maxvar t) 0)
     then decomp_lams_eta_n (n+1) n env body typ
     else rels,c
   in
   let n = List.length rels in
-  let s = list_firstn n s in
-  let l,l' = list_chop n l in
+  let s = List.firstn n s in
+  let l,l' = List.chop n l in
   let t' = type_recomp (l',t') in
   (* The initial ML environment. *)
   let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in
@@ -948,7 +985,7 @@ let extract_fixpoint env vkn (fi,ti,ci) =
   (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
   let sub = List.rev_map mkConst kns in
   for i = 0 to n-1 do
-    if sort_of env ti.(i) <> InProp then begin
+    if sort_of env ti.(i) != InProp then begin
       let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in
       terms.(i) <- e;
       types.(i) <- t;
@@ -988,17 +1025,21 @@ let extract_constant env kn cb =
     | (Info,TypeScheme) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_typ_ax ()
-	  | Def c -> mk_typ (force c)
+	  | Def c -> mk_typ (Mod_subst.force_constr c)
 	  | OpaqueDef c ->
 	    add_opaque r;
-	    if access_opaque () then mk_typ (force_opaque c) else mk_typ_ax ())
+	    if access_opaque () then
+              mk_typ (Opaqueproof.force_proof (Environ.opaque_tables env) c)
+            else mk_typ_ax ())
     | (Info,Default) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_ax ()
-	  | Def c -> mk_def (force c)
+	  | Def c -> mk_def (Mod_subst.force_constr c)
 	  | OpaqueDef c ->
 	    add_opaque r;
-	    if access_opaque () then mk_def (force_opaque c) else mk_ax ())
+	    if access_opaque () then
+              mk_def (Opaqueproof.force_proof (Environ.opaque_tables env) c)
+            else mk_ax ())
 
 let extract_constant_spec env kn cb =
   let r = ConstRef kn in
@@ -1012,27 +1053,32 @@ let extract_constant_spec env kn cb =
 	  | Undef _ | OpaqueDef _ -> Stype (r, vl, None)
 	  | Def body ->
 	      let db = db_from_sign s in
-	      let t = extract_type_scheme env db (force body) (List.length s)
+              let body = Mod_subst.force_constr body in
+	      let t = extract_type_scheme env db body (List.length s)
 	      in Stype (r, vl, Some t))
     | (Info, Default) ->
 	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
+let extract_with_type env c =
+  let typ = type_of env c in
   match flag_of_type env typ with
     | (Info, TypeScheme) ->
 	let s,vl = type_sign_vl env typ in
 	let db = db_from_sign s in
-	let c = match cb.const_body with
-	  | Def body -> force body
-	  (* A "with Definition ..." is necessarily transparent *)
-	  | Undef _ | OpaqueDef _ -> assert false
-	in
 	let t = extract_type_scheme env db c (List.length s) in
 	Some (vl, t)
     | _ -> None
 
+let extract_constr env c =
+  reset_meta_count ();
+  let typ = type_of env c in
+  match flag_of_type env typ with
+    | (_,TypeScheme) -> MLdummy, Tdummy Ktype
+    | (Logic,_) -> MLdummy, Tdummy Kother
+    | (Info,Default) ->
+      let mlt = extract_type env [] 1 typ [] in
+      extract_term env Mlenv.empty mlt c [], mlt
 
 let extract_inductive env kn =
   let ind = extract_ind env kn in
@@ -1043,7 +1089,7 @@ let extract_inductive env kn =
       | [] -> []
       | t::l ->
 	  let l' = filter (succ i) l in
-	  if isDummy (expand env t) || List.mem i implicits then l'
+	  if isDummy (expand env t) || Int.List.mem i implicits then l'
 	  else t::l'
     in filter (1+ind.ind_nparams) l
   in
@@ -1058,9 +1104,9 @@ let logical_decl = function
   | Dterm (_,MLdummy,Tdummy _) -> true
   | Dtype (_,[],Tdummy _) -> true
   | Dfix (_,av,tv) ->
-      (array_for_all ((=) MLdummy) av) &&
-      (array_for_all isDummy tv)
-  | Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
+      (Array.for_all ((==) MLdummy) av) &&
+      (Array.for_all isDummy tv)
+  | Dind (_,i) -> Array.for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false
 
 (*s Is a [ml_spec] logical ? *)
@@ -1068,5 +1114,5 @@ let logical_decl = function
 let logical_spec = function
   | Stype (_, [], Some (Tdummy _)) -> true
   | Sval (_,Tdummy _) -> true
-  | Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
+  | Sind (_,i) -> Array.for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false