Désactivation de dumpglob lors des appels a functional induction (erreurs parasites du Lexer)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11706 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 17 insertions, 9 deletions

diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 5155e614d..49efe362c 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -651,6 +651,7 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
     const::other_result
 
 let build_scheme fas = 
+  Dumpglob.pause ();
   let bodies_types = 
     make_scheme 
       (List.map 
@@ -678,8 +679,9 @@ let build_scheme fas =
 	 (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id
     )
     fas
-    bodies_types
-  
+    bodies_types;
+    Dumpglob.continue ()
+    
 
 
 let build_case_scheme fa = 
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index d7a7c311a..c09c79c18 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -27,10 +27,11 @@ let choose_dest_or_ind scheme_info =
 
 
 let functional_induction with_clean c princl pat =
-  let f,args = decompose_app c in 
-  fun g ->      
-    let princ,bindings, princ_type = 
-      match princl with 
+  Dumpglob.pause ();
+  let res = let f,args = decompose_app c in 
+	      fun g ->      
+		let princ,bindings, princ_type = 
+		  match princl with 
 	| None -> (* No principle is given let's find the good one *)
 	    begin
 	      match kind_of_term f with
@@ -124,6 +125,9 @@ let functional_induction with_clean c princl pat =
          None)
       subst_and_reduce
       g
+  in
+    Dumpglob.continue ();
+    res
       
       
 
@@ -700,7 +704,8 @@ let make_graph (f_ref:global_reference) =
 	| _ -> raise (UserError ("", str "Not a function reference") )
 
   in
-  match c_body.const_body with
+   Dumpglob.pause ();
+  (match c_body.const_body with
     | None -> error "Cannot build a graph over an axiom !"
     | Some b ->
 	let env = Global.env () in
@@ -752,8 +757,9 @@ let make_graph (f_ref:global_reference) =
 	let mp,dp,_ = repr_con c in 
 	List.iter 
 	  (fun ((_,id),_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id))) 
-	  expr_list
-
+	  expr_list);
+  Dumpglob.continue ()
+  
 
 (* let make_graph _ = assert false	 *)