Merge PR #899: [general] Move files to directories so they match linking order.

4 files changed, 0 insertions, 1537 deletions

diff --git a/library/declare.ml b/library/declare.ml
deleted file mode 100644
index 154793a32..000000000
--- a/library/declare.ml
+++ /dev/null
@@ -1,564 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This module is about the low-level declaration of logical objects *)
-
-open Pp
-open CErrors
-open Util
-open Names
-open Libnames
-open Globnames
-open Nameops
-open Term
-open Declarations
-open Entries
-open Libobject
-open Lib
-open Impargs
-open Safe_typing
-open Cooking
-open Decls
-open Decl_kinds
-
-(** flag for internal message display *)
-type internal_flag =
-  | UserAutomaticRequest (* kernel action, a message is displayed *)
-  | InternalTacticRequest  (* kernel action, no message is displayed *)
-  | UserIndividualRequest   (* user action, a message is displayed *)
-
-(** XML output hooks *)
-
-let (f_xml_declare_variable, xml_declare_variable) = Hook.make ~default:ignore ()
-let (f_xml_declare_constant, xml_declare_constant) = Hook.make ~default:ignore ()
-let (f_xml_declare_inductive, xml_declare_inductive) = Hook.make ~default:ignore ()
-
-let if_xml f x = if !Flags.xml_export then f x else ()
-
-(** Declaration of section variables and local definitions *)
-
-type section_variable_entry =
-  | SectionLocalDef of Safe_typing.private_constants definition_entry
-  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
-
-type variable_declaration = DirPath.t * section_variable_entry * logical_kind
-
-let cache_variable ((sp,_),o) =
-  match o with
-  | Inl ctx -> Global.push_context_set false ctx
-  | Inr (id,(p,d,mk)) ->
-  (* Constr raisonne sur les noms courts *)
-  if variable_exists id then
-    alreadydeclared (pr_id id ++ str " already exists");
-
-  let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
-    | SectionLocalAssum ((ty,ctx),poly,impl) ->
-      let () = Global.push_named_assum ((id,ty,poly),ctx) in
-      let impl = if impl then Implicit else Explicit in
-	impl, true, poly, ctx
-    | SectionLocalDef (de) ->
-      let univs = Global.push_named_def (id,de) in
-      Explicit, de.const_entry_opaque,
-      de.const_entry_polymorphic, univs in
-  Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
-  add_section_variable id impl poly ctx;
-  Dischargedhypsmap.set_discharged_hyps sp [];
-  add_variable_data id (p,opaq,ctx,poly,mk)
-
-let discharge_variable (_,o) = match o with
-  | Inr (id,_) ->
-    if variable_polymorphic id then None
-    else Some (Inl (variable_context id))
-  | Inl _ -> Some o
-
-type variable_obj =
-    (Univ.ContextSet.t, Id.t * variable_declaration) union
-
-let inVariable : variable_obj -> obj =
-  declare_object { (default_object "VARIABLE") with
-    cache_function = cache_variable;
-    discharge_function = discharge_variable;
-    classify_function = (fun _ -> Dispose) }
-
-(* for initial declaration *)
-let declare_variable id obj =
-  let oname = add_leaf id (inVariable (Inr (id,obj))) in
-  declare_var_implicits id;
-  Notation.declare_ref_arguments_scope (VarRef id);
-  Heads.declare_head (EvalVarRef id);
-  if_xml (Hook.get f_xml_declare_variable) oname;
-  oname
-
-
-(** Declaration of constants and parameters *)
-
-type constant_obj = {
-  cst_decl : global_declaration;
-  cst_hyps : Dischargedhypsmap.discharged_hyps;
-  cst_kind : logical_kind;
-  cst_locl : bool;
-  mutable cst_exported : Safe_typing.exported_private_constant list;
-  (* mutable: to avoid change the libobject API, since cache_function
-   * does not return an updated object *)
-  mutable cst_was_seff : bool
-}
-
-type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
-
-(* At load-time, the segment starting from the module name to the discharge *)
-(* section (if Remark or Fact) is needed to access a construction *)
-let load_constant i ((sp,kn), obj) =
-  if Nametab.exists_cci sp then
-    alreadydeclared (pr_id (basename sp) ++ str " already exists");
-  let con = Global.constant_of_delta_kn kn in
-  Nametab.push (Nametab.Until i) sp (ConstRef con);
-  add_constant_kind con obj.cst_kind
-
-(* Opening means making the name without its module qualification available *)
-let open_constant i ((sp,kn), obj) =
-  (** Never open a local definition *)
-  if obj.cst_locl then ()
-  else
-    let con = Global.constant_of_delta_kn kn in
-    Nametab.push (Nametab.Exactly i) sp (ConstRef con);
-    match (Global.lookup_constant con).const_body with
-    | (Def _ | Undef _) -> ()
-    | OpaqueDef lc ->
-        match Opaqueproof.get_constraints (Global.opaque_tables ()) lc with
-        | Some f when Future.is_val f ->
-	   Global.push_context_set false (Future.force f)
-        | _ -> ()
-
-let exists_name id =
-  variable_exists id || Global.exists_objlabel (Label.of_id id)
-
-let check_exists sp =
-  let id = basename sp in
-  if exists_name id then alreadydeclared (pr_id id ++ str " already exists")
-
-let cache_constant ((sp,kn), obj) =
-  let id = basename sp in
-  let _,dir,_ = repr_kn kn in
-  let kn' =
-    if obj.cst_was_seff then begin
-      obj.cst_was_seff <- false;  
-      if Global.exists_objlabel (Label.of_id (basename sp))
-      then constant_of_kn kn
-      else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
-    end else
-      let () = check_exists sp in
-      let kn', exported = Global.add_constant dir id obj.cst_decl in
-      obj.cst_exported <- exported;
-      kn' in
-  assert (eq_constant kn' (constant_of_kn kn));
-  Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
-  let cst = Global.lookup_constant kn' in
-  add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
-  Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps;
-  add_constant_kind (constant_of_kn kn) obj.cst_kind
-
-let discharged_hyps kn sechyps =
-  let (_,dir,_) = repr_kn kn in
-  let args = Array.to_list (instance_from_variable_context sechyps) in
-  List.rev_map (Libnames.make_path dir) args
-
-let discharge_constant ((sp, kn), obj) =
-  let con = constant_of_kn kn in
-  let from = Global.lookup_constant con in
-  let modlist = replacement_context () in
-  let hyps,subst,uctx = section_segment_of_constant con in
-  let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in
-  let abstract = (named_of_variable_context hyps, subst, uctx) in
-  let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in
-  Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; }
-
-(* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry = 
-  ConstantEntry
-    (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
-
-let dummy_constant cst = {
-  cst_decl = dummy_constant_entry;
-  cst_hyps = [];
-  cst_kind = cst.cst_kind;
-  cst_locl = cst.cst_locl;
-  cst_exported = [];
-  cst_was_seff = cst.cst_was_seff;
-}
-
-let classify_constant cst = Substitute (dummy_constant cst)
-
-let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) =
-  declare_object_full { (default_object "CONSTANT") with
-    cache_function = cache_constant;
-    load_function = load_constant;
-    open_function = open_constant;
-    classify_function = classify_constant;
-    subst_function = ident_subst_function;
-    discharge_function = discharge_constant }
-
-let declare_scheme = ref (fun _ _ -> assert false)
-let set_declare_scheme f = declare_scheme := f
-
-let declare_constant_common id cst =
-  let update_tables c =
-(*  Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *)
-    declare_constant_implicits c;
-    Heads.declare_head (EvalConstRef c);
-    Notation.declare_ref_arguments_scope (ConstRef c) in
-  let o = inConstant cst in
-  let _, kn as oname = add_leaf id o in
-  List.iter (fun (c,ce,role) ->
-      (* handling of private_constants just exported *)
-      let o = inConstant {
-        cst_decl = ConstantEntry (false, ce);
-        cst_hyps = [] ;
-        cst_kind = IsProof Theorem;
-        cst_locl = false;
-        cst_exported = [];
-        cst_was_seff = true; } in
-      let id = Label.to_id (pi3 (Constant.repr3 c)) in
-      ignore(add_leaf id o);
-      update_tables c;
-      let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in
-      match role with
-      | Safe_typing.Subproof -> ()
-      | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|])
-    (outConstant o).cst_exported;
-  pull_to_head oname;
-  let c = Global.constant_of_delta_kn kn in
-  update_tables c;
-  c
-
-let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
-    ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body =
-  { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
-    const_entry_secctx = None;
-    const_entry_type = types;
-    const_entry_polymorphic = poly;
-    const_entry_universes = univs;
-    const_entry_opaque = opaque;
-    const_entry_feedback = None;
-    const_entry_inline_code = inline}
-
-let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
-  let export = (* We deal with side effects *)
-    match cd with
-    | DefinitionEntry de when
-        export_seff ||
-        not de.const_entry_opaque ||
-        de.const_entry_polymorphic ->
-          let bo = de.const_entry_body in
-          let _, seff = Future.force bo in
-          Safe_typing.empty_private_constants <> seff
-    | _ -> false
-  in
-  let cst = {
-    cst_decl = ConstantEntry (export,cd);
-    cst_hyps = [] ;
-    cst_kind = kind;
-    cst_locl = local;
-    cst_exported = [];
-    cst_was_seff = false;
-  } in
-  let kn = declare_constant_common id cst in
-  let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in
-  kn
-
-let declare_definition ?(internal=UserIndividualRequest)
-  ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
-  ?(poly=false) id ?types (body,ctx) =
-  let cb =
-    definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
-  in
-    declare_constant ~internal ~local id
-      (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
-
-(** Declaration of inductive blocks *)
-
-let declare_inductive_argument_scopes kn mie =
-  List.iteri (fun i {mind_entry_consnames=lc} ->
-    Notation.declare_ref_arguments_scope (IndRef (kn,i));
-    for j=1 to List.length lc do
-      Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j));
-    done) mie.mind_entry_inds
-
-let inductive_names sp kn mie =
-  let (dp,_) = repr_path sp in
-  let kn = Global.mind_of_delta_kn kn in
-  let names, _ =
-    List.fold_left
-      (fun (names, n) ind ->
-	 let ind_p = (kn,n) in
-	 let names, _ =
-	   List.fold_left
-	     (fun (names, p) l ->
-		let sp =
-		  Libnames.make_path dp l
-		in
-		  ((sp, ConstructRef (ind_p,p)) :: names, p+1))
-	     (names, 1) ind.mind_entry_consnames in
-	 let sp = Libnames.make_path dp ind.mind_entry_typename
-	 in
-	   ((sp, IndRef ind_p) :: names, n+1))
-      ([], 0) mie.mind_entry_inds
-  in names
-
-let load_inductive i ((sp,kn),(_,mie)) =
-  let names = inductive_names sp kn mie in
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names
-
-let open_inductive i ((sp,kn),(_,mie)) =
-  let names = inductive_names sp kn mie in
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names
-
-let cache_inductive ((sp,kn),(dhyps,mie)) =
-  let names = inductive_names sp kn mie in
-  List.iter check_exists (List.map fst names);
-  let id = basename sp in
-  let _,dir,_ = repr_kn kn in
-  let kn' = Global.add_mind dir id mie in
-  assert (eq_mind kn' (mind_of_kn kn));
-  let mind = Global.lookup_mind kn' in
-  add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
-  Dischargedhypsmap.set_discharged_hyps sp dhyps;
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
-
-let discharge_inductive ((sp,kn),(dhyps,mie)) =
-  let mind = Global.mind_of_delta_kn kn in
-  let mie = Global.lookup_mind mind in
-  let repl = replacement_context () in
-  let sechyps, _, _ as info = section_segment_of_mutual_inductive mind in
-  Some (discharged_hyps kn sechyps,
-        Discharge.process_inductive info repl mie)
-
-let dummy_one_inductive_entry mie = {
-  mind_entry_typename = mie.mind_entry_typename;
-  mind_entry_arity = mkProp;
-  mind_entry_template = false;
-  mind_entry_consnames = mie.mind_entry_consnames;
-  mind_entry_lc = []
-}
-
-(* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_inductive_entry (_,m) = ([],{
-  mind_entry_params = [];
-  mind_entry_record = None;
-  mind_entry_finite = Decl_kinds.BiFinite;
-  mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
-  mind_entry_universes = Monomorphic_ind_entry Univ.UContext.empty;
-  mind_entry_private = None;
-})
-
-(* reinfer subtyping constraints for inductive after section is dischared. *)
-let infer_inductive_subtyping (pth, mind_ent) =
-  match mind_ent.mind_entry_universes with
-  | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ ->
-    (pth, mind_ent)
-  | Cumulative_ind_entry cumi ->
-    begin
-      let env = Global.env () in
-      let env' =
-        Environ.push_context
-          (Univ.CumulativityInfo.univ_context cumi) env
-      in
-      (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
-      let evd = Evd.from_env env' in
-        (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent)
-    end
-
-type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
-
-let inInductive : inductive_obj -> obj =
-  declare_object {(default_object "INDUCTIVE") with
-    cache_function = cache_inductive;
-    load_function = load_inductive;
-    open_function = open_inductive;
-    classify_function = (fun a -> Substitute (dummy_inductive_entry a));
-    subst_function = ident_subst_function;
-    discharge_function = discharge_inductive;
-    rebuild_function = infer_inductive_subtyping }
-
-let declare_projections mind =
-  let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
-    match spec.mind_record with
-    | Some (Some (_, kns, pjs)) ->
-      Array.iteri (fun i kn ->
-	let id = Label.to_id (Constant.label kn) in
-	let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
-	let kn' = declare_constant id (ProjectionEntry entry,
-				       IsDefinition StructureComponent)
-	in
-	  assert(eq_constant kn kn')) kns; true,true
-    | Some None -> true,false
-    | None -> false,false
-
-(* for initial declaration *)
-let declare_mind mie =
-  let id = match mie.mind_entry_inds with
-    | ind::_ -> ind.mind_entry_typename
-    | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in
-  let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
-  let mind = Global.mind_of_delta_kn kn in
-  let isrecord,isprim = declare_projections mind in
-  declare_mib_implicits mind;
-  declare_inductive_argument_scopes mind mie;
-  if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname);
-  oname, isprim
-
-(* Declaration messages *)
-
-let pr_rank i = pr_nth (i+1)
-
-let fixpoint_message indexes l =
-  Flags.if_verbose Feedback.msg_info (match l with
-  | [] -> anomaly (Pp.str "no recursive definition.")
-  | [id] -> pr_id id ++ str " is recursively defined" ++
-      (match indexes with
-	 | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
-	 | _ -> mt ())
-  | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
-		  spc () ++ str "are recursively defined" ++
-		  match indexes with
-		    | Some a -> spc () ++ str "(decreasing respectively on " ++
-			prvect_with_sep pr_comma pr_rank a ++
-			str " arguments)"
-		    | None -> mt ()))
-
-let cofixpoint_message l =
-  Flags.if_verbose Feedback.msg_info (match l with
-  | [] -> anomaly (Pp.str "No corecursive definition.")
-  | [id] -> pr_id id ++ str " is corecursively defined"
-  | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
-                    spc () ++ str "are corecursively defined"))
-
-let recursive_message isfix i l =
-  (if isfix then fixpoint_message i else cofixpoint_message) l
-
-let definition_message id =
-  Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is defined")
-
-let assumption_message id =
-  (* Changing "assumed" to "declared", "assuming" referring more to
-  the type of the object than to the name of the object (see
-  discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
-  Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is declared")
-
-(** Global universe names, in a different summary *)
-
-type universe_context_decl = polymorphic * Univ.universe_context_set
-
-let cache_universe_context (p, ctx) =
-  Global.push_context_set p ctx;
-  if p then Lib.add_section_context ctx
-
-let input_universe_context : universe_context_decl -> Libobject.obj =
-  declare_object
-    { (default_object "Global universe context state") with
-      cache_function = (fun (na, pi) -> cache_universe_context pi);
-      load_function = (fun _ (_, pi) -> cache_universe_context pi);
-      discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
-      classify_function = (fun a -> Keep a) }
-
-let declare_universe_context poly ctx =
-  Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
-
-(* Discharged or not *)
-type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
-
-let cache_universes (p, l) =
-  let glob = Global.global_universe_names () in
-  let glob', ctx =
-    List.fold_left (fun ((idl,lid),ctx) (id, lev) ->
-        ((Idmap.add id (p, lev) idl,
-          Univ.LMap.add lev id lid),
-         Univ.ContextSet.add_universe lev ctx))
-      (glob, Univ.ContextSet.empty) l
-  in
-  cache_universe_context (p, ctx);
-  Global.set_global_universe_names glob'
-
-let input_universes : universe_decl -> Libobject.obj =
-  declare_object
-    { (default_object "Global universe name state") with
-      cache_function = (fun (na, pi) -> cache_universes pi);
-      load_function = (fun _ (_, pi) -> cache_universes pi);
-      discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
-      classify_function = (fun a -> Keep a) }
-
-let do_universe poly l =
-  let in_section = Lib.sections_are_opened () in
-  let () =
-    if poly && not in_section then
-      user_err ~hdr:"Constraint"
-                   (str"Cannot declare polymorphic universes outside sections")
-  in
-  let l =
-    List.map (fun (l, id) ->
-	      let lev = Universes.new_univ_level (Global.current_dirpath ()) in
-	      (id, lev)) l
-  in
-    Lib.add_anonymous_leaf (input_universes (poly, l))
-
-type constraint_decl = polymorphic * Univ.constraints
-
-let cache_constraints (na, (p, c)) =
-  let ctx =
-    Univ.ContextSet.add_constraints c
-      Univ.ContextSet.empty (* No declared universes here, just constraints *)
-  in cache_universe_context (p,ctx)
-
-let discharge_constraints (_, (p, c as a)) =
-  if p then None else Some a
-
-let input_constraints : constraint_decl -> Libobject.obj =
-  let open Libobject in
-    declare_object
-    { (default_object "Global universe constraints") with
-      cache_function = cache_constraints;
-      load_function = (fun _ -> cache_constraints);
-      discharge_function = discharge_constraints;
-      classify_function = (fun a -> Keep a) }
-
-let do_constraint poly l =
-  let open Misctypes in
-  let u_of_id x =
-    match x with
-    | GProp -> Loc.tag (false, Univ.Level.prop)
-    | GSet  -> Loc.tag (false, Univ.Level.set)
-    | GType None | GType (Some (_, Anonymous)) ->
-       user_err ~hdr:"Constraint"
-                     (str "Cannot declare constraints on anonymous universes")
-    | GType (Some (loc, Name id)) ->
-       let names, _ = Global.global_universe_names () in
-       try loc, Idmap.find id names
-       with Not_found ->
-         user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ pr_id id)
-  in
-  let in_section = Lib.sections_are_opened () in
-  let () =
-    if poly && not in_section then
-      user_err ~hdr:"Constraint"
-                    (str"Cannot declare polymorphic constraints outside sections")
-  in
-  let check_poly ?loc p loc' p' =
-    if poly then ()
-    else if p || p' then
-      let loc = if p then loc else loc' in
-      user_err ?loc ~hdr:"Constraint"
-                    (str "Cannot declare a global constraint on " ++
-                    str "a polymorphic universe, use "
-                    ++ str "Polymorphic Constraint instead")
-  in
-  let constraints = List.fold_left (fun acc (l, d, r) ->
-     let ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in
-     check_poly ?loc:ploc p rloc p';
-     Univ.Constraint.add (lu, d, ru) acc)
-    Univ.Constraint.empty l
-  in
-    Lib.add_anonymous_leaf (input_constraints (poly, constraints))
diff --git a/library/declare.mli b/library/declare.mli
deleted file mode 100644
index 6a0943464..000000000
--- a/library/declare.mli
+++ /dev/null
@@ -1,97 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Libnames
-open Term
-open Entries
-open Decl_kinds
-
-(** This module provides the official functions to declare new variables,
-   parameters, constants and inductive types. Using the following functions
-   will add the entries in the global environment (module [Global]), will
-   register the declarations in the library (module [Lib]) --- so that the
-   reset works properly --- and will fill some global tables such as
-   [Nametab] and [Impargs]. *)
-
-(** Declaration of local constructions (Variable/Hypothesis/Local) *)
-
-type section_variable_entry =
-  | SectionLocalDef of Safe_typing.private_constants definition_entry
-  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
-
-type variable_declaration = DirPath.t * section_variable_entry * logical_kind
-
-val declare_variable : variable -> variable_declaration -> object_name
-
-(** Declaration of global constructions 
-   i.e. Definition/Theorem/Axiom/Parameter/... *)
-
-type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
-
-type internal_flag =
-  | UserAutomaticRequest
-  | InternalTacticRequest
-  | UserIndividualRequest
-
-(* Defaut definition entries, transparent with no secctx or proj information *)
-val definition_entry : ?fix_exn:Future.fix_exn ->
-  ?opaque:bool -> ?inline:bool -> ?types:types ->
-  ?poly:polymorphic -> ?univs:Univ.universe_context ->
-  ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
-
-(** [declare_constant id cd] declares a global declaration
-   (constant/parameter) with name [id] in the current section; it returns
-   the full path of the declaration
-
-  internal specify if the constant has been created by the kernel or by the
-  user, and in the former case, if its errors should be silent *)
-val declare_constant :
- ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
-
-val declare_definition : 
-  ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
-  ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
-  constr Univ.in_universe_context_set -> constant
-
-(** Since transparent constants' side effects are globally declared, we
- *  need that *)
-val set_declare_scheme :
-  (string -> (inductive * constant) array -> unit) -> unit
-
-(** [declare_mind me] declares a block of inductive types with
-   their constructors in the current section; it returns the path of
-   the whole block and a boolean indicating if it is a primitive record. *)
-val declare_mind : mutual_inductive_entry -> object_name * bool
-
-(** Hooks for XML output *)
-val xml_declare_variable : (object_name -> unit) Hook.t
-val xml_declare_constant : (internal_flag * constant -> unit) Hook.t
-val xml_declare_inductive : (bool * object_name -> unit) Hook.t
-
-(** Declaration messages *)
-
-val definition_message : Id.t -> unit
-val assumption_message : Id.t -> unit
-val fixpoint_message : int array option -> Id.t list -> unit
-val cofixpoint_message : Id.t list -> unit
-val recursive_message : bool (** true = fixpoint *) ->
-  int array option -> Id.t list -> unit
-
-val exists_name : Id.t -> bool
-
-
-
-(** Global universe contexts, names and constraints *)
-
-val declare_universe_context : polymorphic -> Univ.universe_context_set -> unit
-
-val do_universe : polymorphic -> Id.t Loc.located list -> unit
-val do_constraint : polymorphic ->
-  (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list ->
-  unit
diff --git a/library/impargs.ml b/library/impargs.ml
deleted file mode 100644
index b7125fc85..000000000
--- a/library/impargs.ml
+++ /dev/null
@@ -1,737 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open CErrors
-open Util
-open Names
-open Globnames
-open Nameops
-open Term
-open Reduction
-open Declarations
-open Environ
-open Libobject
-open Lib
-open Pp
-open Constrexpr
-open Termops
-open Namegen
-open Decl_kinds
-open Context.Named.Declaration
-
-module NamedDecl = Context.Named.Declaration
-
-(*s Flags governing the computation of implicit arguments *)
-
-type implicits_flags = {
-  auto : bool;                     (* automatic or manual only *)
-  strict : bool;                   (* true = strict *)
-  strongly_strict : bool;          (* true = strongly strict *)
-  reversible_pattern : bool;
-  contextual : bool;               (* true = contextual *)
-  maximal : bool
-}
-
-let implicit_args = ref {
-  auto = false;
-  strict = true;
-  strongly_strict = false;
-  reversible_pattern = false;
-  contextual = false;
-  maximal = false;
-}
-
-let make_implicit_args flag =
-  implicit_args := { !implicit_args with auto = flag }
-
-let make_strict_implicit_args flag =
-  implicit_args := { !implicit_args with strict = flag }
-
-let make_strongly_strict_implicit_args flag =
-  implicit_args := { !implicit_args with strongly_strict = flag }
-
-let make_reversible_pattern_implicit_args flag =
-  implicit_args := { !implicit_args with reversible_pattern = flag }
-
-let make_contextual_implicit_args flag =
-  implicit_args := { !implicit_args with contextual = flag }
-
-let make_maximal_implicit_args flag =
-  implicit_args := { !implicit_args with maximal = flag }
-
-let is_implicit_args () = !implicit_args.auto
-let is_strict_implicit_args () = !implicit_args.strict
-let is_strongly_strict_implicit_args () = !implicit_args.strongly_strict
-let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
-let is_contextual_implicit_args () = !implicit_args.contextual
-let is_maximal_implicit_args () = !implicit_args.maximal
-
-let with_implicit_protection f x =
-  let oflags = !implicit_args in
-  try
-    let rslt = f x in
-    implicit_args := oflags;
-    rslt
-  with reraise ->
-    let reraise = CErrors.push reraise in
-    let () = implicit_args := oflags in
-    iraise reraise
-
-let set_maximality imps b =
-  (* Force maximal insertion on ending implicits (compatibility) *)
-  let is_set x = match x with None -> false | _ -> true in
-  b || List.for_all is_set imps
-
-(*s Computation of implicit arguments *)
-
-(* We remember various information about why an argument is
-   inferable as implicit
-
-- [DepRigid] means that the implicit argument can be found by
-  unification along a rigid path (we do not print the arguments of
-  this kind if there is enough arguments to infer them)
-
-- [DepFlex] means that the implicit argument can be found by unification
-  along a collapsable path only (e.g. as x in (P x) where P is another
-  argument) (we do (defensively) print the arguments of this kind)
-
-- [DepFlexAndRigid] means that the least argument from which the
-  implicit argument can be inferred is following a collapsable path
-  but there is a greater argument from where the implicit argument is
-  inferable following a rigid path (useful to know how to print a
-  partial application)
-
-- [Manual] means the argument has been explicitly set as implicit.
-
-  We also consider arguments inferable from the conclusion but it is
-  operational only if [conclusion_matters] is true.
-*)
-
-type argument_position =
-  | Conclusion
-  | Hyp of int
-
-let argument_position_eq p1 p2 = match p1, p2 with
-| Conclusion, Conclusion -> true
-| Hyp h1, Hyp h2 -> Int.equal h1 h2
-| _ -> false
-
-let explicitation_eq ex1 ex2 = match ex1, ex2 with
-| ExplByPos (i1, id1), ExplByPos (i2, id2) ->
-  Int.equal i1 i2 && Option.equal Id.equal id1 id2
-| ExplByName id1, ExplByName id2 ->
-  Id.equal id1 id2
-| _ -> false
-
-type implicit_explanation =
-  | DepRigid of argument_position
-  | DepFlex of argument_position
-  | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
-  | Manual
-
-let argument_less = function
-  | Hyp n, Hyp n' -> n<n'
-  | Hyp _, Conclusion -> true
-  | Conclusion, _ -> false
-
-let update pos rig (na,st) =
-  let e =
-  if rig then
-    match st with
-      | None -> DepRigid pos
-      | Some (DepRigid n as x) ->
-          if argument_less (pos,n) then DepRigid pos else x
-      | Some (DepFlexAndRigid (fpos,rpos) as x) ->
-          if argument_less (pos,fpos) || argument_position_eq pos fpos then DepRigid pos else
-          if argument_less (pos,rpos) then DepFlexAndRigid (fpos,pos) else x
-      | Some (DepFlex fpos) ->
-          if argument_less (pos,fpos) || argument_position_eq pos fpos then DepRigid pos
-          else DepFlexAndRigid (fpos,pos)
-      | Some Manual -> assert false
-  else
-    match st with
-      | None -> DepFlex pos
-      | Some (DepRigid rpos as x) ->
-          if argument_less (pos,rpos) then DepFlexAndRigid (pos,rpos) else x
-      | Some (DepFlexAndRigid (fpos,rpos) as x) ->
-          if argument_less (pos,fpos) then DepFlexAndRigid (pos,rpos) else x
-      | Some (DepFlex fpos as x) ->
-          if argument_less (pos,fpos) then DepFlex pos else x
-      | Some Manual -> assert false
-  in na, Some e
-
-(* modified is_rigid_reference with a truncated env *)
-let is_flexible_reference env bound depth f =
-  match kind_of_term f with
-    | Rel n when n >= bound+depth -> (* inductive type *) false
-    | Rel n when n >= depth -> (* previous argument *) true
-    | Rel n -> (* since local definitions have been expanded *) false
-    | Const (kn,_) ->
-        let cb = Environ.lookup_constant kn env in
-	(match cb.const_body with Def _ -> true | _ -> false)
-    | Var id ->
-        env |> Environ.lookup_named id |> is_local_def
-    | Ind _ | Construct _ -> false
-    |  _ -> true
-
-let push_lift d (e,n) = (push_rel d e,n+1)
-
-let is_reversible_pattern bound depth f l =
-  isRel f && let n = destRel f in (n < bound+depth) && (n >= depth) &&
-  Array.for_all (fun c -> isRel c && destRel c < depth) l &&
-  Array.distinct l
-
-(* Precondition: rels in env are for inductive types only *)
-let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
-  let rec frec rig (env,depth as ed) c =
-    let hd = if strict then whd_all env c else c in
-    let c = if strongly_strict then hd else c in
-    match kind_of_term hd with
-    | Rel n when (n < bound+depth) && (n >= depth) ->
-	let i = bound + depth - n - 1 in
-        acc.(i) <- update pos rig acc.(i)
-    | App (f,l) when revpat && is_reversible_pattern bound depth f l ->
-	let i = bound + depth - destRel f - 1 in
-	acc.(i) <- update pos rig acc.(i)
-    | App (f,_) when rig && is_flexible_reference env bound depth f ->
-	if strict then () else
-          iter_constr_with_full_binders push_lift (frec false) ed c
-    | Proj (p,c) when rig ->
-      if strict then () else
-        iter_constr_with_full_binders push_lift (frec false) ed c	  
-    | Case _ when rig ->
-	if strict then () else
-          iter_constr_with_full_binders push_lift (frec false) ed c
-    | Evar _ -> ()
-    | _ ->
-        iter_constr_with_full_binders push_lift (frec rig) ed c
-  in
-  let () = if not (Vars.noccur_between 1 bound m) then frec true (env,1) m in
-  acc
-
-let rec is_rigid_head t = match kind_of_term t with
-  | Rel _ | Evar _ -> false
-  | Ind _ | Const _ | Var _ | Sort _ -> true
-  | Case (_,_,f,_) -> is_rigid_head f
-  | Proj (p,c) -> true
-  | App (f,args) ->
-      (match kind_of_term f with
-	| Fix ((fi,i),_) -> is_rigid_head (args.(fi.(i)))
-	| _ -> is_rigid_head f)
-  | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _
-  | Prod _ | Meta _ | Cast _ -> assert false
-
-(* calcule la liste des arguments implicites *)
-
-let find_displayed_name_in all avoid na (env, b) =
-  let b = EConstr.of_constr b in
-  let envnames_b = (env, b) in
-  let flag = RenamingElsewhereFor envnames_b in
-  if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b
-  else compute_displayed_name_in Evd.empty flag avoid na b
-
-let compute_implicits_gen strict strongly_strict revpat contextual all env t =
-  let rigid = ref true in
-  let open Context.Rel.Declaration in
-  let rec aux env avoid n names t =
-    let t = whd_all env t in
-    match kind_of_term t with
-      | Prod (na,a,b) ->
-	  let na',avoid' = find_displayed_name_in all avoid na (names,b) in
-	  add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
-            (aux (push_rel (LocalAssum (na',a)) env) avoid' (n+1) (na'::names) b)
-      | _ ->
-	  rigid := is_rigid_head t;
-	  let names = List.rev names in
-	  let v = Array.map (fun na -> na,None) (Array.of_list names) in
-	  if contextual then
-	    add_free_rels_until strict strongly_strict revpat n env t Conclusion v
-	  else v
-  in
-  match kind_of_term (whd_all env t) with
-    | Prod (na,a,b) ->
-	let na',avoid = find_displayed_name_in all [] na ([],b) in
-	let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in
-	!rigid, Array.to_list v
-    | _ -> true, []
-
-let compute_implicits_flags env f all t =
-  compute_implicits_gen
-    (f.strict || f.strongly_strict) f.strongly_strict
-    f.reversible_pattern f.contextual all env t
-
-let compute_auto_implicits env flags enriching t =
-  if enriching then compute_implicits_flags env flags true t
-  else compute_implicits_gen false false false true true env t
-
-let compute_implicits_names env t =
-  let _, impls = compute_implicits_gen false false false false true env t in
-  List.map fst impls
-
-(* Extra information about implicit arguments *)
-
-type maximal_insertion = bool (* true = maximal contextual insertion *)
-type force_inference = bool (* true = always infer, never turn into evar/subgoal *)
-
-type implicit_status =
-    (* None = Not implicit *)
-    (Id.t * implicit_explanation * (maximal_insertion * force_inference)) option
-
-type implicit_side_condition = DefaultImpArgs | LessArgsThan of int
-
-type implicits_list = implicit_side_condition * implicit_status list
-
-let is_status_implicit = function
-  | None -> false
-  | _ -> true
-
-let name_of_implicit = function
-  | None -> anomaly (Pp.str "Not an implicit argument.")
-  | Some (id,_,_) -> id
-
-let maximal_insertion_of = function
-  | Some (_,_,(b,_)) -> b
-  | None -> anomaly (Pp.str "Not an implicit argument.")
-
-let force_inference_of = function
-  | Some (_, _, (_, b)) -> b
-  | None -> anomaly (Pp.str "Not an implicit argument.")
-
-(* [in_ctx] means we know the expected type, [n] is the index of the argument *)
-let is_inferable_implicit in_ctx n = function
-  | None -> false
-  | Some (_,DepRigid (Hyp p),_) -> in_ctx || n >= p
-  | Some (_,DepFlex (Hyp p),_) -> false
-  | Some (_,DepFlexAndRigid (_,Hyp q),_) -> in_ctx || n >= q
-  | Some (_,DepRigid Conclusion,_) -> in_ctx
-  | Some (_,DepFlex Conclusion,_) -> false
-  | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx
-  | Some (_,Manual,_) -> true
-
-let positions_of_implicits (_,impls) =
-  let rec aux n = function
-      [] -> []
-    | Some _ :: l -> n :: aux (n+1) l
-    | None :: l -> aux (n+1) l
-  in aux 1 impls
-
-(* Manage user-given implicit arguments *)
-
-let rec prepare_implicits f = function
-  | [] -> []
-  | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.")
-  | (Name id, Some imp)::imps ->
-      let imps' = prepare_implicits f imps in
-      Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
-  | _::imps -> None :: prepare_implicits f imps
-
-let set_implicit id imp insmax =
-  (id,(match imp with None -> Manual | Some imp -> imp),insmax)
-
-let rec assoc_by_pos k = function
-    (ExplByPos (k', x), b) :: tl when Int.equal k k' -> (x,b), tl
-  | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl
-  | [] -> raise Not_found
-
-let check_correct_manual_implicits autoimps l =
-  List.iter (function
-    | ExplByName id,(b,fi,forced) ->
-	if not forced then
-	  user_err 
-            (str "Wrong or non-dependent implicit argument name: " ++ pr_id id ++ str ".")
-    | ExplByPos (i,_id),_t ->
-	if i<1 || i>List.length autoimps then
-	  user_err 
-            (str "Bad implicit argument number: " ++ int i ++ str ".")
-	else
-	  user_err 
-	    (str "Cannot set implicit argument number " ++ int i ++
-	      str ": it has no name.")) l
-
-let set_manual_implicits env flags enriching autoimps l =
-  let try_forced k l =
-    try
-      let (id, (b, fi, fo)), l' = assoc_by_pos k l in
-	if fo then
-	  let id = match id with Some id -> id | None -> Id.of_string ("arg_" ^ string_of_int k) in
-	    l', Some (id,Manual,(b,fi))
-	else l, None
-    with Not_found -> l, None
-  in
-  if not (List.distinct l) then
-    user_err Pp.(str "Some parameters are referred more than once.");
-  (* Compare with automatic implicits to recover printing data and names *)
-  let rec merge k l = function
-  | (Name id,imp)::imps ->
-      let l',imp,m =
-	try
-          let eq = explicitation_eq in
-	  let (b, fi, fo) = List.assoc_f eq (ExplByName id) l in
-	  List.remove_assoc_f eq (ExplByName id) l, (Some Manual), (Some (b, fi))
-	with Not_found ->
-	try
-	  let (id, (b, fi, fo)), l' = assoc_by_pos k l in
-	    l', (Some Manual), (Some (b,fi))
-	with Not_found ->
-          let m = match enriching, imp with
-          | true, Some _ -> Some (flags.maximal, true)
-          | _ -> None
-          in
-          l, imp, m
-      in
-      let imps' = merge (k+1) l' imps in
-      let m = Option.map (fun (b,f) -> 
-	(* match imp with Some Manual -> (b,f) *)
-	(* | _ ->  *)set_maximality imps' b, f) m in
-      Option.map (set_implicit id imp) m :: imps'
-  | (Anonymous,imp)::imps ->
-      let l', forced = try_forced k l in
-	forced :: merge (k+1) l' imps
-  | [] when begin match l with [] -> true | _ -> false end -> []
-  | [] ->
-      check_correct_manual_implicits autoimps l;
-      []
-  in
-  merge 1 l autoimps
-
-let compute_semi_auto_implicits env f manual t =
-  match manual with
-  | [] ->
-      if not f.auto then [DefaultImpArgs, []]
-      else let _,l = compute_implicits_flags env f false t in
-	     [DefaultImpArgs, prepare_implicits f l]
-  | _ ->
-      let _,autoimpls = compute_auto_implicits env f f.auto t in
-      [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual]
-
-(*s Constants. *)
-
-let compute_constant_implicits flags manual cst =
-  let env = Global.env () in
-  let cb = Environ.lookup_constant cst env in
-  let ty = Typeops.type_of_constant_type env cb.const_type in
-  let impls = compute_semi_auto_implicits env flags manual ty in
-    impls
-
-(*s Inductives and constructors. Their implicit arguments are stored
-   in an array, indexed by the inductive number, of pairs $(i,v)$ where
-   $i$ are the implicit arguments of the inductive and $v$ the array of
-   implicit arguments of the constructors. *)
-
-let compute_mib_implicits flags manual kn =
-  let env = Global.env () in
-  let mib = lookup_mind kn env in
-  let ar =
-    Array.to_list
-      (Array.mapi  (* No need to lift, arities contain no de Bruijn *)
-        (fun i mip ->
-	  (** No need to care about constraints here *)
-	  let ty, _ = Global.type_of_global_in_context env (IndRef (kn,i)) in
-	  Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty))
-        mib.mind_packets) in
-  let env_ar = push_rel_context ar env in
-  let imps_one_inductive i mip =
-    let ind = (kn,i) in
-    let ar, _ = Global.type_of_global_in_context env (IndRef ind) in
-    ((IndRef ind,compute_semi_auto_implicits env flags manual ar),
-     Array.mapi (fun j c ->
-       (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar flags manual c))
-       mip.mind_nf_lc)
-  in
-  Array.mapi imps_one_inductive mib.mind_packets
-
-let compute_all_mib_implicits flags manual kn =
-  let imps = compute_mib_implicits flags manual kn in
-  List.flatten
-    (Array.map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps)
-
-(*s Variables. *)
-
-let compute_var_implicits flags manual id =
-  let env = Global.env () in
-  compute_semi_auto_implicits env flags manual (NamedDecl.get_type (lookup_named id env))
-
-(* Implicits of a global reference. *)
-
-let compute_global_implicits flags manual = function
-  | VarRef id -> compute_var_implicits flags manual id
-  | ConstRef kn -> compute_constant_implicits flags manual kn
-  | IndRef (kn,i) ->
-      let ((_,imps),_) = (compute_mib_implicits flags manual kn).(i) in imps
-  | ConstructRef ((kn,i),j) ->
-      let (_,cimps) = (compute_mib_implicits flags manual kn).(i) in snd cimps.(j-1)
-
-(* Merge a manual explicitation with an implicit_status list *)
-
-let merge_impls (cond,oldimpls) (_,newimpls) =
-  let oldimpls,usersuffiximpls = List.chop (List.length newimpls) oldimpls in
-  cond, (List.map2 (fun orig ni ->
-    match orig with
-    | Some (_, Manual, _) -> orig
-    | _ -> ni) oldimpls newimpls)@usersuffiximpls
-
-(* Caching implicits *)
-
-type implicit_interactive_request =
-  | ImplAuto
-  | ImplManual of int
-
-type implicit_discharge_request =
-  | ImplLocal
-  | ImplConstant of constant * implicits_flags
-  | ImplMutualInductive of mutual_inductive * implicits_flags
-  | ImplInteractive of global_reference * implicits_flags *
-      implicit_interactive_request
-
-let implicits_table = Summary.ref Refmap.empty ~name:"implicits"
-
-let implicits_of_global ref =
-  try
-    let l = Refmap.find ref !implicits_table in
-    try
-      let rename_l = Arguments_renaming.arguments_names ref in
-      let rec rename implicits names = match implicits, names with
-        | [], _ -> []
-        | _, [] -> implicits
-        | Some (_, x,y) :: implicits, Name id :: names ->
-           Some (id, x,y) :: rename implicits names
-        | imp :: implicits, _ :: names -> imp :: rename implicits names
-      in
-      List.map (fun (t, il) -> t, rename il rename_l) l
-    with Not_found -> l
-  with Not_found -> [DefaultImpArgs,[]]
-
-let cache_implicits_decl (ref,imps) =
-  implicits_table := Refmap.add ref imps !implicits_table
-
-let load_implicits _ (_,(_,l)) = List.iter cache_implicits_decl l
-
-let cache_implicits o =
-  load_implicits 1 o
-
-let subst_implicits_decl subst (r,imps as o) =
-  let r' = fst (subst_global subst r) in if r==r' then o else (r',imps)
-
-let subst_implicits (subst,(req,l)) =
-  (ImplLocal,List.smartmap (subst_implicits_decl subst) l)
-
-let impls_of_context ctx =
-  let map (decl, impl) = match impl with
-  | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true))
-  | _ -> None
-  in
-  List.rev_map map (List.filter (fst %> is_local_assum) ctx)
-
-let adjust_side_condition p = function
-  | LessArgsThan n -> LessArgsThan (n+p)
-  | DefaultImpArgs -> DefaultImpArgs
-
-let add_section_impls vars extra_impls (cond,impls) =
-  let p = List.length vars - List.length extra_impls in
-  adjust_side_condition p cond, extra_impls @ impls
-
-let discharge_implicits (_,(req,l)) =
-  match req with
-  | ImplLocal -> None
-  | ImplInteractive (ref,flags,exp) ->
-    (try
-      let vars = variable_section_segment_of_reference ref in
-      let ref' = if isVarRef ref then ref else pop_global_reference ref in
-      let extra_impls = impls_of_context vars in
-      let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
-      Some (ImplInteractive (ref',flags,exp),l')
-    with Not_found -> (* ref not defined in this section *) Some (req,l))
-  | ImplConstant (con,flags) ->
-    (try
-      let con' = pop_con con in
-      let vars,_,_ = section_segment_of_constant con in
-      let extra_impls = impls_of_context vars in
-      let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in
-      let l' = [ConstRef con',newimpls] in
-	Some (ImplConstant (con',flags),l')
-    with Not_found -> (* con not defined in this section *) Some (req,l))
-  | ImplMutualInductive (kn,flags) ->
-    (try
-      let l' = List.map (fun (gr, l) ->
-	let vars = variable_section_segment_of_reference gr in
-	let extra_impls = impls_of_context vars in
-	((if isVarRef gr then gr else pop_global_reference gr),
-	 List.map (add_section_impls vars extra_impls) l)) l
-      in
-	Some (ImplMutualInductive (pop_kn kn,flags),l')
-    with Not_found -> (* ref not defined in this section *) Some (req,l))
-
-let rebuild_implicits (req,l) =
-  match req with
-  | ImplLocal -> assert false
-  | ImplConstant (con,flags) ->
-      let oldimpls = snd (List.hd l) in
-      let newimpls = compute_constant_implicits flags [] con in
-      req, [ConstRef con, List.map2 merge_impls oldimpls newimpls]
-  | ImplMutualInductive (kn,flags) ->
-      let newimpls = compute_all_mib_implicits flags [] kn in
-      let rec aux olds news =
-	match olds, news with
-	| (_, oldimpls) :: old, (gr, newimpls) :: tl ->
-	    (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl
-	| [], [] -> []
-	| _, _ -> assert false
-      in req, aux l newimpls
-
-  | ImplInteractive (ref,flags,o) ->
-      (if isVarRef ref && is_in_section ref then ImplLocal else req),
-      match o with
-      | ImplAuto ->
-	  let oldimpls = snd (List.hd l) in
-	  let newimpls = compute_global_implicits flags [] ref in
-	    [ref,List.map2 merge_impls oldimpls newimpls]
-      | ImplManual userimplsize ->
-	  let oldimpls = snd (List.hd l) in
-	  if flags.auto then
-	    let newimpls = List.hd (compute_global_implicits flags [] ref) in
-	    let p = List.length (snd newimpls) - userimplsize in
-	    let newimpls = on_snd (List.firstn p) newimpls in
-	    [ref,List.map (fun o -> merge_impls o newimpls) oldimpls]
-	  else
-	    [ref,oldimpls]
-
-let classify_implicits (req,_ as obj) = match req with
-| ImplLocal -> Dispose
-| _ -> Substitute obj
-
-type implicits_obj =
-    implicit_discharge_request *
-      (global_reference * implicits_list list) list
-
-let inImplicits : implicits_obj -> obj =
-  declare_object {(default_object "IMPLICITS") with
-    cache_function = cache_implicits;
-    load_function = load_implicits;
-    subst_function = subst_implicits;
-    classify_function = classify_implicits;
-    discharge_function = discharge_implicits;
-    rebuild_function = rebuild_implicits }
-
-let is_local local ref = local || isVarRef ref && is_in_section ref
-
-let declare_implicits_gen req flags ref =
-  let imps = compute_global_implicits flags [] ref in
-  add_anonymous_leaf (inImplicits (req,[ref,imps]))
-
-let declare_implicits local ref =
-  let flags = { !implicit_args with auto = true } in
-  let req =
-    if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in
-    declare_implicits_gen req flags ref
-
-let declare_var_implicits id =
-  let flags = !implicit_args in
-    declare_implicits_gen ImplLocal flags (VarRef id)
-
-let declare_constant_implicits con =
-  let flags = !implicit_args in
-    declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con)
-
-let declare_mib_implicits kn =
-  let flags = !implicit_args in
-  let imps = Array.map_to_list
-    (fun (ind,cstrs) -> ind::(Array.to_list cstrs))
-    (compute_mib_implicits flags [] kn) in
-    add_anonymous_leaf
-      (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
-
-(* Declare manual implicits *)
-type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool)
-
-type manual_implicits = manual_explicitation list
-
-let compute_implicits_with_manual env typ enriching l =
-  let _,autoimpls = compute_auto_implicits env !implicit_args enriching typ in
-  set_manual_implicits env !implicit_args enriching autoimpls l
-
-let check_inclusion l =
-  (* Check strict inclusion *)
-  let rec aux = function
-    | n1::(n2::_ as nl) ->
-	if n1 <= n2 then
-	  user_err Pp.(str "Sequences of implicit arguments must be of different lengths.");
-	aux nl
-    | _ -> () in
-  aux (List.map (fun (imps,_) -> List.length imps) l)
-
-let check_rigidity isrigid =
-  if not isrigid then
-    user_err  (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.")
-
-let projection_implicits env p impls = 
-  let pb = Environ.lookup_projection p env in
-    CList.skipn_at_least pb.Declarations.proj_npars impls
-
-let declare_manual_implicits local ref ?enriching l =
-  let flags = !implicit_args in
-  let env = Global.env () in
-  let t, _ = Global.type_of_global_in_context (Global.env ()) ref in
-  let enriching = Option.default flags.auto enriching in
-  let isrigid,autoimpls = compute_auto_implicits env flags enriching t in
-  let l' = match l with
-    | [] -> assert false
-    | [l] ->
-	[DefaultImpArgs, set_manual_implicits env flags enriching autoimpls l]
-    | _ ->
-	check_rigidity isrigid;
-	let l = List.map (fun imps -> (imps,List.length imps)) l in
-	let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in
-	check_inclusion l;
-	let nargs = List.length autoimpls in
-	List.map (fun (imps,n) ->
-	  (LessArgsThan (nargs-n),
-	   set_manual_implicits env flags enriching autoimpls imps)) l in
-  let req =
-    if is_local local ref then ImplLocal
-    else ImplInteractive(ref,flags,ImplManual (List.length autoimpls))
-  in
-    add_anonymous_leaf (inImplicits (req,[ref,l']))
-
-let maybe_declare_manual_implicits local ref ?enriching l =
-  match l with
-  | [] -> ()
-  | _ -> declare_manual_implicits local ref ?enriching [l]
-
-let extract_impargs_data impls =
-  let rec aux p = function
-    | (DefaultImpArgs, imps)::_ -> [None,imps]
-    | (LessArgsThan n, imps)::l -> (Some (p,n),imps) :: aux (n+1) l
-    | [] -> [] in
-  aux 0 impls
-
-let lift_implicits n =
-  List.map (fun x ->
-    match fst x with
-	ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
-      | _ -> x)
-
-let make_implicits_list l = [DefaultImpArgs, l]
-
-let rec drop_first_implicits p l =
-  if Int.equal p 0 then l else match l with
-  | _,[] as x -> x
-  | DefaultImpArgs,imp::impls ->
-      drop_first_implicits (p-1) (DefaultImpArgs,impls)
-  | LessArgsThan n,imp::impls ->
-      let n = if is_status_implicit imp then n-1 else n in
-      drop_first_implicits (p-1) (LessArgsThan n,impls)
-
-let rec select_impargs_size n = function
-  | [] -> [] (* Tolerance for (DefaultImpArgs,[]) *)
-  | [_, impls] | (DefaultImpArgs, impls)::_ -> impls
-  | (LessArgsThan p, impls)::l ->
-      if n <= p then impls else select_impargs_size n l
-
-let select_stronger_impargs = function
-  | [] -> [] (* Tolerance for (DefaultImpArgs,[]) *)
-  | (_,impls)::_ -> impls
diff --git a/library/impargs.mli b/library/impargs.mli
deleted file mode 100644
index 4b78f54ea..000000000
--- a/library/impargs.mli
+++ /dev/null
@@ -1,139 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Globnames
-open Term
-open Environ
-
-(** {6 Implicit Arguments } *)
-(** Here we store the implicit arguments. Notice that we
-    are outside the kernel, which knows nothing about implicit arguments. *)
-
-val make_implicit_args : bool -> unit
-val make_strict_implicit_args : bool -> unit
-val make_strongly_strict_implicit_args : bool -> unit
-val make_reversible_pattern_implicit_args : bool -> unit
-val make_contextual_implicit_args : bool -> unit
-val make_maximal_implicit_args : bool -> unit
-
-val is_implicit_args : unit -> bool
-val is_strict_implicit_args : unit -> bool
-val is_strongly_strict_implicit_args : unit -> bool
-val is_reversible_pattern_implicit_args : unit -> bool
-val is_contextual_implicit_args : unit -> bool
-val is_maximal_implicit_args : unit -> bool
-
-val with_implicit_protection : ('a -> 'b) -> 'a -> 'b
-
-(** {6 ... } *)
-(** An [implicits_list] is a list of positions telling which arguments
-    of a reference can be automatically infered *)
-
-
-type argument_position =
-  | Conclusion
-  | Hyp of int
-
-(** We remember various information about why an argument is
-   inferable as implicit *)
-type implicit_explanation =
-  | DepRigid of argument_position
-      (** means that the implicit argument can be found by
-	  unification along a rigid path (we do not print the arguments of
-	  this kind if there is enough arguments to infer them) *)
-  | DepFlex of argument_position
-      (** means that the implicit argument can be found by unification
-	  along a collapsable path only (e.g. as x in (P x) where P is another
-	  argument) (we do (defensively) print the arguments of this kind) *)
-  | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
-      (** means that the least argument from which the
-	  implicit argument can be inferred is following a collapsable path
-	  but there is a greater argument from where the implicit argument is
-	  inferable following a rigid path (useful to know how to print a
-	  partial application) *)
-  | Manual
-      (** means the argument has been explicitly set as implicit. *)
-
-(**  We also consider arguments inferable from the conclusion but it is
-     operational only if [conclusion_matters] is true. *)
-
-type maximal_insertion = bool (** true = maximal contextual insertion *)
-type force_inference = bool (** true = always infer, never turn into evar/subgoal *)
-
-type implicit_status = (Id.t * implicit_explanation * 
-			  (maximal_insertion * force_inference)) option
-    (** [None] = Not implicit *)
-
-type implicit_side_condition
-
-type implicits_list = implicit_side_condition * implicit_status list
-
-val is_status_implicit : implicit_status -> bool
-val is_inferable_implicit : bool -> int -> implicit_status -> bool
-val name_of_implicit : implicit_status -> Id.t
-val maximal_insertion_of : implicit_status -> bool
-val force_inference_of : implicit_status -> bool
-
-val positions_of_implicits : implicits_list -> int list
-
-(** A [manual_explicitation] is a tuple of a positional or named explicitation with
-   maximal insertion, force inference and force usage flags. Forcing usage makes
-   the argument implicit even if the automatic inference considers it not inferable. *)
-type manual_explicitation = Constrexpr.explicitation *
-    (maximal_insertion * force_inference * bool)
-
-type manual_implicits = manual_explicitation list
-
-val compute_implicits_with_manual : env -> types -> bool ->
-  manual_implicits -> implicit_status list
-
-val compute_implicits_names : env -> types -> Name.t list
-
-(** {6 Computation of implicits (done using the global environment). } *)
-
-val declare_var_implicits : variable -> unit
-val declare_constant_implicits : constant -> unit
-val declare_mib_implicits : mutual_inductive -> unit
-
-val declare_implicits : bool -> global_reference -> unit
-
-(** [declare_manual_implicits local ref enriching l]
-   Manual declaration of which arguments are expected implicit.
-   If not set, we decide if it should enrich by automatically inferd
-   implicits depending on the current state.
-   Unsets implicits if [l] is empty. *)
-
-val declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
-  manual_implicits list -> unit
-
-(** If the list is empty, do nothing, otherwise declare the implicits. *)
-
-val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
-  manual_implicits -> unit
-
-val implicits_of_global : global_reference -> implicits_list list
-
-val extract_impargs_data :
-  implicits_list list -> ((int * int) option * implicit_status list) list
-
-val lift_implicits : int -> manual_implicits -> manual_implicits
-
-val make_implicits_list : implicit_status list -> implicits_list list
-
-val drop_first_implicits : int -> implicits_list -> implicits_list
-
-val projection_implicits : env -> projection -> implicit_status list -> 
-  implicit_status list
-
-val select_impargs_size : int -> implicits_list list -> implicit_status list
-
-val select_stronger_impargs : implicits_list list -> implicit_status list
-
-val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool
-(** Equality on [explicitation]. *)