5 files changed, 37 insertions, 42 deletions
diff --git a/library/global.ml b/library/global.ml
index 3781ff3230..bfea6d3dea 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -128,19 +128,7 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
 
 let opaque_tables () = Environ.opaque_tables (env ())
 
-let instantiate cb c =
-  let open Declarations in
-  match cb.const_universes with
-  | Monomorphic_const _ -> c, Univ.AUContext.empty
-  | Polymorphic_const ctx -> c, ctx
-
-let body_of_constant_body cb =
-  let open Declarations in
-  let otab = opaque_tables () in
-  match cb.const_body with
-  | Undef _ -> None
-  | Def c -> Some (instantiate cb (Mod_subst.force_constr c))
-  | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o))
+let body_of_constant_body ce = body_of_constant_body (env ()) ce
 
 let body_of_constant cst = body_of_constant_body (lookup_constant cst)
 
@@ -165,8 +153,6 @@ let import c u d = globalize (Safe_typing.import c u d)
 let env_of_context hyps =
   reset_with_named_context hyps (env())
 
-open Globnames
-
 let constr_of_global_in_context = Typeops.constr_of_global_in_context
 let type_of_global_in_context = Typeops.type_of_global_in_context
 
@@ -175,21 +161,9 @@ let universes_of_global gr =
 
 let is_polymorphic r = Environ.is_polymorphic (env()) r
 
-let is_template_polymorphic r = 
-  let env = env() in 
-  match r with
-  | VarRef id -> false
-  | ConstRef c -> false
-  | IndRef ind -> Environ.template_polymorphic_ind ind env
-  | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env
-
-let is_type_in_type r =
-  let env = env() in
-  match r with
-  | VarRef id -> false
-  | ConstRef c -> Environ.type_in_type_constant c env
-  | IndRef ind -> Environ.type_in_type_ind ind env
-  | ConstructRef cstr -> Environ.type_in_type_ind (inductive_of_constructor cstr) env
+let is_template_polymorphic r = is_template_polymorphic (env ()) r
+
+let is_type_in_type r = is_type_in_type (env ()) r
 
 let current_modpath () =
   Safe_typing.current_modpath (safe_env ())
@@ -208,11 +182,7 @@ let register field value =
 let register_inline c = globalize0 (Safe_typing.register_inline c)
 
 let set_strategy k l =
-  GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l)
-
-let set_reduction_sharing b =
-  let env = safe_env () in
-  let flags = Environ.typing_flags (Safe_typing.env_of_safe_env env) in
-  let flags = { flags with Declarations.share_reduction = b } in
-  let env = Safe_typing.set_typing_flags flags env in
-  GlobalSafeEnv.set_safe_env env
+  globalize0 (Safe_typing.set_strategy k l)
+
+let set_share_reduction b =
+  globalize0 (Safe_typing.set_share_reduction b)
diff --git a/library/global.mli b/library/global.mli
index 42a8005a4f..762a3f006d 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -150,7 +150,9 @@ val register_inline : Constant.t -> unit
 
 val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit
 
-val set_reduction_sharing : bool -> unit
+(** {6 Conversion settings } *)
+
+val set_share_reduction : bool -> unit
 
 (* Modifies the global state, registering new universes *)
 
diff --git a/library/libobject.ml b/library/libobject.ml
index ea19fbb90b..43934304c2 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -71,7 +71,7 @@ type dynamic_object_declaration = {
 let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t
 
 let cache_tab =
-  (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
+  (Hashtbl.create 223 : (string,dynamic_object_declaration) Hashtbl.t)
 
 let declare_object_full odecl =
   let na = odecl.object_name in
diff --git a/library/nametab.ml b/library/nametab.ml
index 06ace373c3..029d850504 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -74,6 +74,8 @@ module type NAMETREE = sig
   val user_name : qualid -> t -> user_name
   val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
+  (** Matches a prefix of [qualid], useful for completion *)
+  val match_prefixes : qualid -> t -> elt list
 end
 
 module Make (U : UserName) (E : EqualityType) : NAMETREE
@@ -259,9 +261,19 @@ let find_prefixes qid tab =
     search_prefixes (Id.Map.find id tab) (DirPath.repr dir)
   with Not_found -> []
 
-end
-
+let match_prefixes =
+  let cprefix x y = CString.(compare x (sub y 0 (min (length x) (length y)))) in
+  fun qid tab ->
+    try
+      let (dir,id) = repr_qualid qid in
+      let id_prefix = cprefix Id.(to_string id) in
+      let matches = Id.Map.filter_range (fun x -> id_prefix Id.(to_string x)) tab in
+      let matches = Id.Map.mapi (fun _key tab -> search_prefixes tab (DirPath.repr dir)) matches in
+      (* Coq's flatten is "magical", so this is not so bad perf-wise *)
+      CList.flatten @@ Id.Map.(fold (fun _ r l -> r :: l) matches [])
+    with Not_found -> []
 
+end
 
 (* Global name tables *************************************************)
 
@@ -447,6 +459,10 @@ let locate_extended_all_dir qid = DirTab.find_prefixes qid !the_dirtab
 
 let locate_extended_all_modtype qid = MPTab.find_prefixes qid !the_modtypetab
 
+(* Completion *)
+let completion_canditates qualid =
+  ExtRefTab.match_prefixes qualid !the_ccitab
+
 (* Derived functions *)
 
 let locate_constant qid =
diff --git a/library/nametab.mli b/library/nametab.mli
index 1c3322bfb1..1e479b200b 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -118,6 +118,12 @@ val locate_extended_all : qualid -> extended_global_reference list
 val locate_extended_all_dir : qualid -> global_dir_reference list
 val locate_extended_all_modtype : qualid -> ModPath.t list
 
+(** Experimental completion support, API is _unstable_ *)
+val completion_canditates : qualid -> extended_global_reference list
+(** [completion_canditates qualid] will return the list of global
+    references that have [qualid] as a prefix. UI usually will want to
+    compose this with [shortest_qualid_of_global] *)
+
 (** Mapping a full path to a global reference *)
 
 val global_of_path : full_path -> GlobRef.t
@@ -211,6 +217,7 @@ module type NAMETREE = sig
   val user_name : qualid -> t -> user_name
   val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
+  val match_prefixes : qualid -> t -> elt list
 end
 
 module Make (U : UserName) (E : EqualityType) :