diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/gen_principle.ml | 18 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 2 |
3 files changed, 11 insertions, 11 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 60717c6eec..352b21a15a 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1170,7 +1170,7 @@ let get_funs_constant mp = in l_const -let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Proof_global.proof_entry list = +let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Declare.proof_entry list = let exception Found_type of int in let env = Global.env () in let funs = List.map fst fas in @@ -1244,7 +1244,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef | Some equation -> Declareops.is_opaque (Global.lookup_constant equation) in - let const = {const with Proof_global.proof_entry_opaque = opacity } in + let const = {const with Declare.proof_entry_opaque = opacity } in (* The others are just deduced *) if List.is_empty other_princ_types then @@ -1255,8 +1255,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef let sorts = Array.of_list sorts in List.map (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types in - let open Proof_global in - let first_princ_body,first_princ_type = const.proof_entry_body, const.proof_entry_type in + let first_princ_body,first_princ_type = Declare.(const.proof_entry_body, const.proof_entry_type) in let ctxt,fix = Term.decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = Constr.destFix fix in let other_result = @@ -1299,10 +1298,10 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef let princ_body = Termops.it_mkLambda_or_LetIn (Constr.mkFix((idxs,i),decl)) ctxt in - {const with - proof_entry_body = - (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects)); - proof_entry_type = Some scheme_type + { const with + Declare.proof_entry_body = + (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects)); + proof_entry_type = Some scheme_type } ) other_fun_princ_types @@ -1358,7 +1357,8 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) = Array.of_list (List.map (fun entry -> - (EConstr.of_constr (fst (fst(Future.force entry.Proof_global.proof_entry_body))), EConstr.of_constr (Option.get entry.Proof_global.proof_entry_type )) + (EConstr.of_constr (fst (fst (Future.force entry.Declare.proof_entry_body))), + EConstr.of_constr (Option.get entry.Declare.proof_entry_type )) ) (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs)) ) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 7719705138..ba37b9b461 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -115,7 +115,7 @@ 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 fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in let r = match scope with | Discharge -> let c = SectionLocalDef const in diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 16beaaa3c7..34fb10bb67 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -44,7 +44,7 @@ val make_eq : unit -> EConstr.constr val save : Id.t - -> Evd.side_effects Proof_global.proof_entry + -> Evd.side_effects Declare.proof_entry -> ?hook:DeclareDef.Hook.t -> UState.t -> DeclareDef.locality |