From 1235c6c3cfc6770920f46de30b1c4b0f5cb44b19 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 28 Oct 2015 12:49:03 +0100
Subject: Do not pause globing in funind. (Fix bug #4382)

Since the functions of this plugin exit by raising exceptions, globing
was never restarted. This prevented coqdoc from generating a proper
output whenever some feature of this plugin was used. There does not seem
to be any parsing of dynamic expressions, so pausing globing does not make
much sense in the first place.
---
 plugins/funind/functional_principles_types.ml | 7 +------
 plugins/funind/indfun.ml                      | 9 ++-------
 2 files changed, 3 insertions(+), 13 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 64284c6fe7..9e27ddf2e9 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -594,9 +594,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
     in
     const::other_result
 
-	   
 let build_scheme fas =
-  Dumpglob.pause ();
   let evd = (ref (Evd.from_env (Global.env ()))) in
   let pconstants = (List.map
 	 (fun (_,f,sort) ->
@@ -626,10 +624,7 @@ let build_scheme fas =
        Declare.definition_message princ_id
     )
     fas
-    bodies_types;
-    Dumpglob.continue ()
-
-
+    bodies_types
 
 let build_case_scheme fa =
   let env = Global.env ()
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index eadeebd38e..47c67ed2aa 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -27,7 +27,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 ->
@@ -123,9 +122,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
@@ -831,7 +828,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 ->
@@ -883,8 +879,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
 
-- 
cgit v1.2.3