Merge branch 'v8.5'

1 files changed, 3 insertions, 8 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index ab3629f89e..bf9da870e4 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -28,7 +28,6 @@ let choose_dest_or_ind scheme_info =
   Tactics.induction_destruct (is_rec_info scheme_info) false
 
 let functional_induction with_clean c princl pat =
-  Dumpglob.pause ();
   let res =
     let f,args = decompose_app c in
     fun g ->
@@ -124,9 +123,7 @@ let functional_induction with_clean c princl pat =
 	 (args_as_induction_constr,princ')))
       subst_and_reduce
       g'
-  in
-    Dumpglob.continue ();
-    res
+  in res
 
 let rec abstract_glob_constr c = function
   | [] -> c
@@ -596,7 +593,7 @@ let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ
 
 let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = 
   let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
-  let ((_,_,typel),ctx,_) = Command.interp_fixpoint fixl ntns in
+  let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in
   let constr_expr_typel = 
     with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx))) typel in
   let fixpoint_exprl_with_new_bl = 
@@ -832,7 +829,6 @@ let make_graph (f_ref:global_reference) =
 	  end
       | _ -> raise (UserError ("", str "Not a function reference") )
   in
-  Dumpglob.pause ();
   (match Global.body_of_constant_body c_body with
      | None -> error "Cannot build a graph over an axiom !"
      | Some body ->
@@ -884,8 +880,7 @@ let make_graph (f_ref:global_reference) =
 	 (* We register the infos *)
 	 List.iter
 	   (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id)))
-	   expr_list);
-  Dumpglob.continue ()
+	   expr_list)
 
 let do_generate_principle = do_generate_principle [] warning_error true