Merge branch 'v8.5'

3 files changed, 16 insertions, 24 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d41ecebe0d..66f1ecd786 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -235,11 +235,9 @@ let compile_files () =
 
 (*s options for the virtual machine *)
 
-let boxed_val = ref false
 let use_vm = ref false
 
 let set_vm_opt () =
-  Vm.set_transp_values (not !boxed_val);
   Vconv.set_use_vm !use_vm
 
 (** Options for proof general *)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 836de042bf..406aacebea 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -463,19 +463,6 @@ let map_replace k v m = ProgMap.add k (Ephemeron.create v) (ProgMap.remove k m)
 
 let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
 
-let map_cardinal m =
-  let i = ref 0 in
-    ProgMap.iter (fun _ _ -> incr i) m;
-    !i
-
-exception Found of program_info
-
-let map_first m =
-  try
-    ProgMap.iter (fun _ v -> raise (Found v)) m;
-    assert(false)
-  with Found x -> x
-
 let from_prg : program_info ProgMap.t ref =
   Summary.ref ProgMap.empty ~name:"program-tcc-table"
 
@@ -682,6 +669,22 @@ let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls
       prg_hook = hook;
       prg_opaque = opaque; }
 
+let map_cardinal m =
+  let i = ref 0 in
+  ProgMap.iter (fun _ v ->
+		if snd (Ephemeron.get v).prg_obligations > 0 then incr i) m;
+  !i
+
+exception Found of program_info
+
+let map_first m =
+  try
+    ProgMap.iter (fun _ v ->
+		  if snd (Ephemeron.get v).prg_obligations > 0 then
+		    raise (Found v)) m;
+    assert(false)
+  with Found x -> x
+
 let get_prog name =
   let prg_infos = !from_prg in
     match name with
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d0e231b264..8efe3614e2 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1375,15 +1375,6 @@ let _ =
       optread  = (fun () -> !Closure.share);
       optwrite = (fun b -> Closure.share := b) }
 
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "use of boxed values";
-      optkey   = ["Boxed";"Values"];
-      optread  = (fun _ -> not (Vm.transp_values ()));
-      optwrite = (fun b -> Vm.set_transp_values (not b)) }
-
 (* No more undo limit in the new proof engine.
    The command still exists for compatibility (e.g. with ProofGeneral) *)