diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 81 |
1 files changed, 37 insertions, 44 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 40f66ce5eb..17c79e0e6c 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -49,10 +49,10 @@ let filter_map filter f = let rec it = function | [] -> [] | e::l -> - if filter e - then - (f e) :: it l - else it l + if filter e + then + (f e) :: it l + else it l in it @@ -62,12 +62,12 @@ let chop_rlambda_n = if n == 0 then List.rev acc,rt else - match DAst.get rt with - | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b - | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b - | _ -> - raise (CErrors.UserError(Some "chop_rlambda_n", - str "chop_rlambda_n: Not enough Lambdas")) + match DAst.get rt with + | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b + | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b + | _ -> + raise (CErrors.UserError(Some "chop_rlambda_n", + str "chop_rlambda_n: Not enough Lambdas")) in chop_lambda_n [] @@ -76,9 +76,9 @@ let chop_rprod_n = if n == 0 then List.rev acc,rt else - match DAst.get rt with - | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b - | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) + match DAst.get rt with + | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b + | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) in chop_prod_n [] @@ -115,35 +115,28 @@ let eq = lazy(EConstr.of_constr (coq_constant "eq")) let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl")) (*****************************************************************) -(* Copy of the standart save mechanism but without the much too *) +(* Copy of the standard save mechanism but without the much too *) (* slow reduction function *) (*****************************************************************) -open Entries open Decl_kinds open Declare let definition_message = Declare.definition_message -let get_locality = function -| Discharge -> true -| Local -> true -| Global -> false - let save id const ?hook uctx (locality,_,kind) = - let fix_exn = Future.fix_exn_of const.const_entry_body in - let l,r = match locality with - | Discharge when Lib.sections_are_opened () -> + let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in + let r = match locality with + | Discharge -> let k = Kindops.logical_kind_of_goal_kind kind in - let c = SectionLocalDef const in - let _ = declare_variable id (Lib.cwd(), c, k) in - (Local, VarRef id) - | Discharge | Local | Global -> - let local = get_locality locality in + let c = SectionLocalDef const in + let _ = declare_variable id (Lib.cwd(), c, k) in + VarRef id + | Global local -> let k = Kindops.logical_kind_of_goal_kind kind in - let kn = declare_constant id ~local (DefinitionEntry const, k) in - (locality, ConstRef kn) + let kn = declare_constant id ~local (Declare.DefinitionEntry const, k) in + ConstRef kn in - Lemmas.call_hook ?hook ~fix_exn uctx [] l r; + DeclareDef.Hook.call ?hook ~fix_exn uctx [] locality r; definition_message id let with_full_print f a = @@ -172,14 +165,14 @@ let with_full_print f a = res with | reraise -> - Impargs.make_implicit_args old_implicit_args; - Impargs.make_strict_implicit_args old_strict_implicit_args; - Impargs.make_contextual_implicit_args old_contextual_implicit_args; - Flags.raw_print := old_rawprint; - Constrextern.print_universes := old_printuniverses; + Impargs.make_implicit_args old_implicit_args; + Impargs.make_strict_implicit_args old_strict_implicit_args; + Impargs.make_contextual_implicit_args old_contextual_implicit_args; + Flags.raw_print := old_rawprint; + Constrextern.print_universes := old_printuniverses; Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; - Dumpglob.continue (); - raise reraise + Dumpglob.continue (); + raise reraise @@ -219,8 +212,8 @@ let rec do_cache_info finfo = function else if finfo'.function_constant = finfo.function_constant then finfo::finfos else - let res = do_cache_info finfo finfos in - if res == finfos then l else finfo'::l + let res = do_cache_info finfo finfos in + if res == finfos then l else finfo'::l let cache_Function (_,(finfos)) = @@ -324,7 +317,7 @@ let find_Function_of_graph ind = let update_Function finfo = (* Pp.msgnl (pr_info finfo); *) Lib.add_anonymous_leaf (in_Function finfo) - + let add_Function is_general f = let f_id = Label.to_id (Constant.label f) in @@ -357,12 +350,12 @@ let add_Function is_general f = let pr_table env sigma = pr_table env sigma !from_function (*********************************) -(* Debuging *) +(* Debugging *) let functional_induction_rewrite_dependent_proofs = ref true let function_debug = ref false open Goptions -let functional_induction_rewrite_dependent_proofs_sig = +let functional_induction_rewrite_dependent_proofs_sig = { optdepr = false; optname = "Functional Induction Rewrite Dependent"; @@ -386,7 +379,7 @@ let function_debug_sig = let () = declare_bool_option function_debug_sig -let do_observe () = !function_debug +let do_observe () = !function_debug |