1 files changed, 11 insertions, 7 deletions
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index caa9b328a0..f51586c739 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -12,6 +12,8 @@ open Util
 open Vernacexpr
 open Context.Named.Declaration
 
+module NamedDecl = Context.Named.Declaration
+
 let to_string e =
   let rec aux = function
     | SsEmpty -> "()"
@@ -35,12 +37,14 @@ let in_nameset =
 let rec close_fwd e s =
   let s' =
     List.fold_left (fun s decl ->
-      let (id,b,ty) = Context.Named.Declaration.to_tuple decl in
-      let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in
-      let vty = global_vars_set e ty in
+      let vb = match decl with
+               | LocalAssum _ -> Id.Set.empty
+               | LocalDef (_,b,_) -> global_vars_set e b
+      in
+      let vty = global_vars_set e (NamedDecl.get_type decl) in
       let vbty = Id.Set.union vb vty in
       if Id.Set.exists (fun v -> Id.Set.mem v s) vbty
-      then Id.Set.add id (Id.Set.union s vbty) else s)
+      then Id.Set.add (NamedDecl.get_id decl) (Id.Set.union s vbty) else s)
     s (named_context e)
     in
   if Id.Set.equal s s' then s else close_fwd e s'
@@ -63,13 +67,13 @@ and set_of_id env ty id =
         Id.Set.union (global_vars_set env ty) acc)
       Id.Set.empty ty
   else if Id.to_string id = "All" then
-    List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty
+    List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
   else if CList.mem_assoc_f Id.equal id !known_names then
     process_expr env (CList.assoc_f Id.equal id !known_names) []
   else Id.Set.singleton id
 
 and full_set env =
-  List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty
+  List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
 
 let process_expr env e ty =
   let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in
@@ -104,7 +108,7 @@ let remove_ids_and_lets env s ids =
 let suggest_Proof_using name env vars ids_typ context_ids =
   let module S = Id.Set in
   let open Pp in
-  let print x = prerr_endline (string_of_ppcmds x) in
+  let print x = Feedback.msg_error x in
   let pr_set parens s =
     let wrap ppcmds =
       if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"