diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 48 |
1 files changed, 8 insertions, 40 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 52a29fb559..80fc64fe65 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -40,7 +40,9 @@ let locate_constant ref = let locate_with_msg msg f x = try f x - with Not_found -> raise (CErrors.UserError(None, msg)) + with + | Not_found -> + CErrors.user_err msg let filter_map filter f = @@ -64,8 +66,7 @@ let chop_rlambda_n = | 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")) + CErrors.user_err ~hdr:"chop_rlambda_n" (str "chop_rlambda_n: Not enough Lambdas") in chop_lambda_n [] @@ -76,7 +77,8 @@ let chop_rprod_n = 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")) + | _ -> + CErrors.user_err ~hdr:"chop_rprod_n" (str "chop_rprod_n: Not enough products") in chop_prod_n [] @@ -92,13 +94,6 @@ let list_union_eq eq_fun l1 l2 = let list_add_set_eq eq_fun x l = if List.exists (eq_fun x) l then l else x::l -let const_of_id id = - let princ_ref = qualid_of_ident id in - try Constrintern.locate_reference princ_ref - with Not_found -> - CErrors.user_err ~hdr:"IndFun.const_of_id" - (str "cannot find " ++ Id.print id) - [@@@ocaml.warning "-3"] let coq_constant s = UnivGen.constr_of_monomorphic_global @@ @@ -112,29 +107,6 @@ let find_reference sl s = let eq = lazy(EConstr.of_constr (coq_constant "eq")) let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl")) -(*****************************************************************) -(* Copy of the standard save mechanism but without the much too *) -(* slow reduction function *) -(*****************************************************************) -open Declare -open DeclareDef - -let definition_message = Declare.definition_message - -let save name const ?hook uctx scope kind = - let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in - let r = match scope with - | Discharge -> - let c = SectionLocalDef const in - let () = declare_variable ~name ~kind c in - GlobRef.VarRef name - | Global local -> - let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in - GlobRef.ConstRef kn - in - DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r }); - definition_message name - let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () and old_strict_implicit_args = Impargs.is_strict_implicit_args () @@ -301,20 +273,16 @@ let find_or_none id = ) with Not_found -> None - - let find_Function_infos f = - Cmap_env.find f !from_function - + Cmap_env.find_opt f !from_function let find_Function_of_graph ind = - Indmap.find ind !from_graph + Indmap.find_opt ind !from_graph 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 let equation_lemma = find_or_none (mk_equation_id f_id) |