diff options
| -rw-r--r-- | contrib/funind/functional_principles_types.ml | 6 | ||||
| -rw-r--r-- | contrib/funind/indfun.ml | 20 |
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 *) |