diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 6 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 23 |
5 files changed, 20 insertions, 19 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 2c5118e928..4f32bbd99d 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -935,7 +935,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let f_def = Global.lookup_constant (destConst f) in let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in let f_body = - force (Option.get f_def.const_body) + force (Option.get (body_of_constant f_def)) in let params,f_body_with_params = decompose_lam_n nb_params f_body in let (_,num),(_,_,bodies) = destFix f_body_with_params in @@ -1051,7 +1051,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : } in let get_body const = - match (Global.lookup_constant const ).const_body with + match body_of_constant (Global.lookup_constant const) with | Some b -> let body = force b in Tacred.cbv_norm_flags diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 1d089409b0..2ba29ced7a 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -445,7 +445,7 @@ let get_funs_constant mp dp = in function const -> let find_constant_body const = - match (Global.lookup_constant const ).const_body with + match body_of_constant (Global.lookup_constant const) with | Some b -> let body = force b in let body = Tacred.cbv_norm_flags @@ -579,7 +579,7 @@ let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition let finfos = find_Function_infos this_block_funs.(0) in try let equation = Option.get finfos.equation_lemma in - (Global.lookup_constant equation).Declarations.const_opaque + Declarations.is_opaque (Global.lookup_constant equation) with Option.IsNone -> (* non recursive definition *) false in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 38492f88b5..dd48765fb5 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -834,7 +834,7 @@ let make_graph (f_ref:global_reference) = | _ -> raise (UserError ("", str "Not a function reference") ) in Dumpglob.pause (); - (match c_body.const_body with + (match body_of_constant c_body with | None -> error "Cannot build a graph over an axiom !" | Some b -> let env = Global.env () in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 1de0f91d15..094d2e50fd 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -120,9 +120,9 @@ let const_of_id id = let def_of_const t = match (Term.kind_of_term t) with Term.Const sp -> - (try (match (Global.lookup_constant sp) with - {Declarations.const_body=Some c} -> Declarations.force c - |_ -> assert false) + (try (match Declarations.body_of_constant (Global.lookup_constant sp) with + | Some c -> Declarations.force c + | _ -> assert false) with _ -> assert false) |_ -> assert false diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 4217b83faf..11fbc01baf 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -136,9 +136,9 @@ let message s = if Flags.is_verbose () then msgnl(str s);; let def_of_const t = match (kind_of_term t) with Const sp -> - (try (match (Global.lookup_constant sp) with - {const_body=Some c} -> Declarations.force c - |_ -> assert false) + (try (match body_of_constant (Global.lookup_constant sp) with + | Some c -> Declarations.force c + | _ -> assert false) with _ -> anomaly ("Cannot find definition of constant "^ (string_of_id (id_of_label (con_label sp)))) @@ -939,6 +939,13 @@ let build_new_goal_type () = let res = build_and_l sub_gls_types in res +let is_opaque_constant c = + let cb = Global.lookup_constant c in + match cb.Declarations.const_body with + | Declarations.OpaqueDef _ -> true + | Declarations.Undef _ -> true + | Declarations.Def _ -> false + let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) let current_proof_name = get_current_proof_name () in @@ -958,10 +965,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ let na_ref = Libnames.Ident (dummy_loc,na) in let na_global = Nametab.global na_ref in match na_global with - ConstRef c -> - let cb = Global.lookup_constant c in - if cb.Declarations.const_opaque then true - else begin match cb.const_body with None -> true | _ -> false end + ConstRef c -> is_opaque_constant c | _ -> anomaly "equation_lemma: not a constant" in let lemma = mkConst (Lib.make_con na) in @@ -1339,10 +1343,7 @@ let (com_eqn : int -> identifier -> fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type -> let opacity = match terminate_ref with - | ConstRef c -> - let cb = Global.lookup_constant c in - if cb.Declarations.const_opaque then true - else begin match cb.const_body with None -> true | _ -> false end + | ConstRef c -> is_opaque_constant c | _ -> anomaly "terminate_lemma: not a constant" in let (evmap, env) = Lemmas.get_current_context() in |