From c951e2ed88437c613bd4355b32547f9c39269eed Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 20 Aug 2019 00:02:28 +0200 Subject: [declare] Move proof_entry type to declare, put interactive proof data on top of declare. This PR is a follow up to #10406 , moving the then introduced `proof_entry` type to `Declare`. This makes sense as `Declare` is the main consumer of the entry type, and already provides the constructors for it. This is a step towards making the entry type private, which will allow us to enforce / handle invariants on entry data better. A side-effect of this PR is that now `Proof_global` does depend on `Declare`, not the other way around, but that makes sense given that closing an interactive proof will be a client of declare. Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into tactics due to `abstract`, at some point we may be able to unify all them into a single file in `vernac`. --- .../10674-ejgallego-proofs+declare_unif.sh | 6 + plugins/funind/gen_principle.ml | 18 +- plugins/funind/indfun_common.ml | 2 +- plugins/funind/indfun_common.mli | 2 +- proofs/pfedit.ml | 195 ------------- proofs/pfedit.mli | 89 ------ proofs/proof_global.ml | 314 --------------------- proofs/proof_global.mli | 121 -------- proofs/proofs.mllib | 2 - tactics/abstract.ml | 10 +- tactics/abstract.mli | 4 +- tactics/declare.ml | 21 +- tactics/declare.mli | 19 +- tactics/ind_tables.ml | 2 +- tactics/pfedit.ml | 195 +++++++++++++ tactics/pfedit.mli | 89 ++++++ tactics/proof_global.ml | 303 ++++++++++++++++++++ tactics/proof_global.mli | 103 +++++++ tactics/tactics.mllib | 2 + vernac/comDefinition.ml | 4 +- vernac/comDefinition.mli | 2 +- vernac/declareDef.ml | 2 +- vernac/declareDef.mli | 4 +- vernac/declareObl.ml | 9 +- vernac/declareObl.mli | 2 +- vernac/indschemes.ml | 1 - vernac/lemmas.ml | 22 +- vernac/obligations.ml | 4 +- vernac/record.ml | 1 - 29 files changed, 771 insertions(+), 777 deletions(-) create mode 100644 dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh delete mode 100644 proofs/pfedit.ml delete mode 100644 proofs/pfedit.mli delete mode 100644 proofs/proof_global.ml delete mode 100644 proofs/proof_global.mli create mode 100644 tactics/pfedit.ml create mode 100644 tactics/pfedit.mli create mode 100644 tactics/proof_global.ml create mode 100644 tactics/proof_global.mli diff --git a/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh new file mode 100644 index 0000000000..6dc44aa627 --- /dev/null +++ b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10674" ] || [ "$CI_BRANCH" = "proofs+declare_unif" ]; then + + equations_CI_REF=proofs+declare_unif + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi 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 diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml deleted file mode 100644 index 99a254652c..0000000000 --- a/proofs/pfedit.ml +++ /dev/null @@ -1,195 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* !use_unification_heuristics_ref); - optwrite = (fun a -> use_unification_heuristics_ref:=a); -}) - -let use_unification_heuristics () = !use_unification_heuristics_ref - -exception NoSuchGoal -let () = CErrors.register_handler begin function - | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") - | _ -> raise CErrors.Unhandled -end - -let get_nth_V82_goal p i = - let Proof.{ sigma; goals } = Proof.data p in - try { it = List.nth goals (i-1) ; sigma } - with Failure _ -> raise NoSuchGoal - -let get_goal_context_gen pf i = - let { it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in - (sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) - -let get_goal_context pf i = - let p = Proof_global.get_proof pf in - get_goal_context_gen p i - -let get_current_goal_context pf = - let p = Proof_global.get_proof pf in - try get_goal_context_gen p 1 - with - | NoSuchGoal -> - (* spiwack: returning empty evar_map, since if there is no goal, - under focus, there is no accessible evar either. EJGA: this - seems strange, as we have pf *) - let env = Global.env () in - Evd.from_env env, env - -let get_current_context pf = - let p = Proof_global.get_proof pf in - try get_goal_context_gen p 1 - with - | NoSuchGoal -> - (* No more focused goals *) - let { Proof.sigma } = Proof.data p in - sigma, Global.env () - -let solve ?with_end_tac gi info_lvl tac pr = - let tac = match with_end_tac with - | None -> tac - | Some etac -> Proofview.tclTHEN tac etac in - let tac = match info_lvl with - | None -> tac - | Some _ -> Proofview.Trace.record_info_trace tac - in - let nosuchgoal = Proofview.tclZERO (Proof_bullet.SuggestNoSuchGoals (1,pr)) in - let tac = let open Goal_select in match gi with - | SelectAlreadyFocused -> - let open Proofview.Notations in - Proofview.numgoals >>= fun n -> - if n == 1 then tac - else - let e = CErrors.UserError - (None, - Pp.(str "Expected a single focused goal but " ++ - int n ++ str " goals are focused.")) - in - Proofview.tclZERO e - - | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac - | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac - | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac - | SelectAll -> tac - in - let tac = - if use_unification_heuristics () then - Proofview.tclTHEN tac Refine.solve_constraints - else tac - in - let env = Global.env () in - let (p,(status,info),()) = Proof.run_tactic env tac pr in - let env = Global.env () in - let sigma = Evd.from_env env in - let () = - match info_lvl with - | None -> () - | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info env sigma ~lvl:i info)) - in - (p,status) - -let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None tac) - -(**********************************************************************) -(* Shortcut to build a term using tactics *) - -let next = let n = ref 0 in fun () -> incr n; !n - -let build_constant_by_tactic ~name ctx sign ~poly typ tac = - let evd = Evd.from_ctx ctx in - let goals = [ (Global.env_of_context sign , typ) ] in - let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in - try - let pf, status = by tac pf in - let open Proof_global in - let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in - match entries with - | [entry] -> - let univs = UState.demote_seff_univs entry.Proof_global.proof_entry_universes universes in - entry, status, univs - | _ -> - CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") - with reraise -> - let reraise = CErrors.push reraise in - iraise reraise - -let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = - let name = Id.of_string ("temporary_proof"^string_of_int (next())) in - let sign = val_of_named_context (named_context env) in - let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in - let body, eff = Future.force ce.Proof_global.proof_entry_body in - let (cb, ctx) = - if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) - else body - in - let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in - cb, status, univs - -let refine_by_tactic ~name ~poly env sigma ty tac = - (* Save the initial side-effects to restore them afterwards. We set the - current set of side-effects to be empty so that we can retrieve the - ones created during the tactic invocation easily. *) - let eff = Evd.eval_side_effects sigma in - let sigma = Evd.drop_side_effects sigma in - (* Save the existing goals *) - let prev_future_goals = save_future_goals sigma in - (* Start a proof *) - let prf = Proof.start ~name ~poly sigma [env, ty] in - let (prf, _, ()) = - try Proof.run_tactic env tac prf - with Logic_monad.TacticFailure e as src -> - (* Catch the inner error of the monad tactic *) - let (_, info) = CErrors.push src in - iraise (e, info) - in - (* Plug back the retrieved sigma *) - let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in - assert (stack = []); - let ans = match Proofview.initial_goals entry with - | [c, _] -> c - | _ -> assert false - in - let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in - (* [neff] contains the freshly generated side-effects *) - let neff = Evd.eval_side_effects sigma in - (* Reset the old side-effects *) - let sigma = Evd.drop_side_effects sigma in - let sigma = Evd.emit_side_effects eff sigma in - (* Restore former goals *) - let sigma = restore_future_goals sigma prev_future_goals in - (* Push remaining goals as future_goals which is the only way we - have to inform the caller that there are goals to collect while - not being encapsulated in the monad *) - (* Goals produced by tactic "shelve" *) - let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in - (* Goals produced by tactic "give_up" *) - let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in - (* Other goals *) - let sigma = List.fold_right Evd.declare_future_goal goals sigma in - (* Get rid of the fresh side-effects by internalizing them in the term - itself. Note that this is unsound, because the tactic may have solved - other goals that were already present during its invocation, so that - those goals rely on effects that are not present anymore. Hopefully, - this hack will work in most cases. *) - let neff = neff.Evd.seff_private in - let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in - ans, sigma diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli deleted file mode 100644 index 0626e40047..0000000000 --- a/proofs/pfedit.mli +++ /dev/null @@ -1,89 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* int -> Evd.evar_map * env - -(** [get_current_goal_context ()] works as [get_goal_context 1] *) -val get_current_goal_context : Proof_global.t -> Evd.evar_map * env - -(** [get_current_context ()] returns the context of the - current focused goal. If there is no focused goal but there - is a proof in progress, it returns the corresponding evar_map. - If there is no pending proof then it returns the current global - environment and empty evar_map. *) -val get_current_context : Proof_global.t -> Evd.evar_map * env - -(** {6 ... } *) - -(** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th - subgoal of the current focused proof. [solve SelectAll - tac] applies [tac] to all subgoals. *) - -val solve : ?with_end_tac:unit Proofview.tactic -> - Goal_select.t -> int option -> unit Proofview.tactic -> - Proof.t -> Proof.t * bool - -(** [by tac] applies tactic [tac] to the 1st subgoal of the current - focused proof. - Returns [false] if an unsafe tactic has been used. *) - -val by : unit Proofview.tactic -> Proof_global.t -> Proof_global.t * bool - -(** Option telling if unification heuristics should be used. *) -val use_unification_heuristics : unit -> bool - -(** [build_by_tactic typ tac] returns a term of type [typ] by calling - [tac]. The return boolean, if [false] indicates the use of an unsafe - tactic. *) - -val build_constant_by_tactic - : name:Id.t - -> UState.t - -> named_context_val - -> poly:bool - -> EConstr.types - -> unit Proofview.tactic - -> Evd.side_effects Proof_global.proof_entry * bool * UState.t - -val build_by_tactic - : ?side_eff:bool - -> env - -> UState.t - -> poly:bool - -> EConstr.types - -> unit Proofview.tactic - -> constr * bool * UState.t - -val refine_by_tactic - : name:Id.t - -> poly:bool - -> env -> Evd.evar_map - -> EConstr.types - -> unit Proofview.tactic - -> constr * Evd.evar_map -(** A variant of the above function that handles open terms as well. - Caveat: all effects are purged in the returned term at the end, but other - evars solved by side-effects are NOT purged, so that unexpected failures may - occur. Ideally all code using this function should be rewritten in the - monad. *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml deleted file mode 100644 index 851a3d1135..0000000000 --- a/proofs/proof_global.ml +++ /dev/null @@ -1,314 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* Proofview.tclUNIT () - | Some tac -> - let open Geninterp in - let {Proof.poly} = Proof.data ps.proof in - let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in - let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in - let tac = Geninterp.interp tag ist tac in - Ftactic.run tac (fun _ -> Proofview.tclUNIT ()) - in - let (newpr,ret) = f et ps.proof in - let ps = { ps with proof = newpr } in - ps, ret - -let compact_the_proof pf = map_proof Proof.compact pf - -(* Sets the tactic to be used when a tactic line is closed with [...] *) -let set_endline_tactic tac ps = - { ps with endline_tactic = Some tac } - -(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of - name [name] with goals [goals] (a list of pairs of environment and - conclusion). The proof is started in the evar map [sigma] (which - can typically contain universe constraints), and with universe - bindings [udecl]. *) -let start_proof ~name ~udecl ~poly sigma goals = - let proof = Proof.start ~name ~poly sigma goals in - let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in - { proof - ; endline_tactic = None - ; section_vars = None - ; udecl - ; initial_euctx - } - -let start_dependent_proof ~name ~udecl ~poly goals = - let proof = Proof.dependent_start ~name ~poly goals in - let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in - { proof - ; endline_tactic = None - ; section_vars = None - ; udecl - ; initial_euctx - } - -let get_used_variables pf = pf.section_vars -let get_universe_decl pf = pf.udecl - -let set_used_variables ps l = - let open Context.Named.Declaration in - let env = Global.env () in - let ids = List.fold_right Id.Set.add l Id.Set.empty in - let ctx = Environ.keep_hyps env ids in - let ctx_set = - List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in - let vars_of = Environ.global_vars_set in - let aux env entry (ctx, all_safe as orig) = - match entry with - | LocalAssum ({binder_name=x},_) -> - if Id.Set.mem x all_safe then orig - else (ctx, all_safe) - | LocalDef ({binder_name=x},bo, ty) as decl -> - if Id.Set.mem x all_safe then orig else - let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in - if Id.Set.subset vars all_safe - then (decl :: ctx, Id.Set.add x all_safe) - else (ctx, all_safe) in - let ctx, _ = - Environ.fold_named_context aux env ~init:(ctx,ctx_set) in - if not (Option.is_empty ps.section_vars) then - CErrors.user_err Pp.(str "Used section variables can be declared only once"); - (* EJGA: This is always empty thus we should modify the type *) - (ctx, []), { ps with section_vars = Some ctx} - -let get_open_goals ps = - let Proof.{ goals; stack; shelf } = Proof.data ps.proof in - List.length goals + - List.fold_left (+) 0 - (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + - List.length shelf - -type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t - -let private_poly_univs = - let b = ref true in - let _ = Goptions.(declare_bool_option { - optdepr = false; - optname = "use private polymorphic universes for Qed constants"; - optkey = ["Private";"Polymorphic";"Universes"]; - optread = (fun () -> !b); - optwrite = ((:=) b); - }) - in - fun () -> !b - -let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now - (fpl : closed_proof_output Future.computation) ps = - let { section_vars; proof; udecl; initial_euctx } = ps in - let Proof.{ name; poly; entry } = Proof.data proof in - let opaque = match opaque with Opaque -> true | Transparent -> false in - let constrain_variables ctx = - UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx - in - let fpl, univs = Future.split2 fpl in - let universes = if poly || now then Future.force univs else initial_euctx in - (* Because of dependent subgoals at the beginning of proofs, we could - have existential variables in the initial types of goals, we need to - normalise them for the kernel. *) - let subst_evar k = - let { Proof.sigma } = Proof.data proof in - Evd.existential_opt_value0 sigma k in - let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar - (UState.subst universes) in - - let make_body = - if poly || now then - let make_body t (c, eff) = - let body = c in - let allow_deferred = - not poly && (keep_body_ucst_separate || - not (Safe_typing.empty_private_constants = eff.Evd.seff_private)) - in - let typ = if allow_deferred then t else nf t in - let used_univs_body = Vars.universes_of_constr body in - let used_univs_typ = Vars.universes_of_constr typ in - if allow_deferred then - let initunivs = UState.univ_entry ~poly initial_euctx in - let ctx = constrain_variables universes in - (* For vi2vo compilation proofs are computed now but we need to - complement the univ constraints of the typ with the ones of - the body. So we keep the two sets distinct. *) - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx_body = UState.restrict ctx used_univs in - let univs = UState.check_mono_univ_decl ctx_body udecl in - (initunivs, typ), ((body, univs), eff) - else if poly && opaque && private_poly_univs () then - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let universes = UState.restrict universes used_univs in - let typus = UState.restrict universes used_univs_typ in - let udecl = UState.check_univ_decl ~poly typus udecl in - let ubody = Univ.ContextSet.diff - (UState.context_set universes) - (UState.context_set typus) - in - (udecl, typ), ((body, ubody), eff) - else - (* Since the proof is computed now, we can simply have 1 set of - constraints in which we merge the ones for the body and the ones - for the typ. We recheck the declaration after restricting with - the actually used universes. - TODO: check if restrict is really necessary now. *) - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx = UState.restrict universes used_univs in - let univs = UState.check_univ_decl ~poly ctx udecl in - (univs, typ), ((body, Univ.ContextSet.empty), eff) - in - fun t p -> Future.split2 (Future.chain p (make_body t)) - else - fun t p -> - (* Already checked the univ_decl for the type universes when starting the proof. *) - let univctx = UState.univ_entry ~poly:false universes in - let t = nf t in - Future.from_val (univctx, t), - Future.chain p (fun (pt,eff) -> - (* Deferred proof, we already checked the universe declaration with - the initial universes, ensure that the final universes respect - the declaration as well. If the declaration is non-extensible, - this will prevent the body from adding universes and constraints. *) - let univs = Future.force univs in - let univs = constrain_variables univs in - let used_univs = Univ.LSet.union - (Vars.universes_of_constr t) - (Vars.universes_of_constr pt) - in - let univs = UState.restrict univs used_univs in - let univs = UState.check_mono_univ_decl univs udecl in - (pt,univs),eff) - in - let entry_fn p (_, t) = - let t = EConstr.Unsafe.to_constr t in - let univstyp, body = make_body t p in - let univs, typ = Future.force univstyp in - { - proof_entry_body = body; - proof_entry_secctx = section_vars; - proof_entry_feedback = feedback_id; - proof_entry_type = Some typ; - proof_entry_inline_code = false; - proof_entry_opaque = opaque; - proof_entry_universes = univs; } - in - let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in - { name; entries = entries; poly; universes; udecl } - -let return_proof ?(allow_partial=false) ps = - let { proof } = ps in - if allow_partial then begin - let proofs = Proof.partial_proof proof in - let Proof.{sigma=evd} = Proof.data proof in - let eff = Evd.eval_side_effects evd in - (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate - side-effects... This may explain why one need to uniquize side-effects - thereafter... *) - let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in - proofs, Evd.evar_universe_context evd - end else - let Proof.{name=pid;entry} = Proof.data proof in - let initial_goals = Proofview.initial_goals entry in - let evd = Proof.return ~pid proof in - let eff = Evd.eval_side_effects evd in - let evd = Evd.minimize_universes evd in - let proof_opt c = - match EConstr.to_constr_opt evd c with - | Some p -> p - | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain") - in - (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate - side-effects... This may explain why one need to uniquize side-effects - thereafter... *) - (* EJGA: actually side-effects de-duplication and this codepath is - unrelated. Duplicated side-effects arise from incorrect scheme - generation code, the main bulk of it was mostly fixed by #9836 - but duplication can still happen because of rewriting schemes I - think; however the code below is mostly untested, the only - code-paths that generate several proof entries are derive and - equations and so far there is no code in the CI that will - actually call those and do a side-effect, TTBOMK *) - let proofs = - List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in - proofs, Evd.evar_universe_context evd - -let close_future_proof ~opaque ~feedback_id ps proof = - close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps - -let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps = - close_proof ~opaque ~keep_body_ucst_separate ~now:true - (Future.from_val ~fix_exn (return_proof ps)) ps - -let update_global_env = - map_proof (fun p -> - let { Proof.sigma } = Proof.data p in - let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in - let p, (status,info), _ = Proof.run_tactic (Global.env ()) tac p in - p) diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli deleted file mode 100644 index 54d5c2087a..0000000000 --- a/proofs/proof_global.mli +++ /dev/null @@ -1,121 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* Proof.t -val get_proof_name : t -> Names.Id.t -val get_used_variables : t -> Constr.named_context option - -(** Get the universe declaration associated to the current proof. *) -val get_universe_decl : t -> UState.universe_decl - -(** Get initial universe state *) -val get_initial_euctx : t -> UState.t - -val compact_the_proof : t -> t - -(** When a proof is closed, it is reified into a [proof_object], where - [id] is the name of the proof, [entries] the list of the proof terms - (in a form suitable for definitions). Together with the [terminator] - function which takes a [proof_object] together with a [proof_end] - (i.e. an proof ending command) and registers the appropriate - values. *) -type 'a proof_entry = { - proof_entry_body : 'a Entries.const_entry_body; - (* List of section variables *) - proof_entry_secctx : Constr.named_context option; - (* State id on which the completion of type checking is reported *) - proof_entry_feedback : Stateid.t option; - proof_entry_type : Constr.types option; - proof_entry_universes : Entries.universes_entry; - proof_entry_opaque : bool; - proof_entry_inline_code : bool; -} - -(** When a proof is closed, it is reified into a [proof_object] *) -type proof_object = - { name : Names.Id.t - (** name of the proof *) - ; entries : Evd.side_effects proof_entry list - (** list of the proof terms (in a form suitable for definitions). *) - ; poly : bool - (** polymorphic status *) - ; universes: UState.t - (** universe state *) - ; udecl : UState.universe_decl - (** universe declaration *) - } - -type opacity_flag = Opaque | Transparent - -(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of - name [name] with goals [goals] (a list of pairs of environment and - conclusion); [poly] determines if the proof is universe - polymorphic. The proof is started in the evar map [sigma] (which - can typically contain universe constraints), and with universe - bindings [udecl]. *) -val start_proof - : name:Names.Id.t - -> udecl:UState.universe_decl - -> poly:bool - -> Evd.evar_map - -> (Environ.env * EConstr.types) list - -> t - -(** Like [start_proof] except that there may be dependencies between - initial goals. *) -val start_dependent_proof - : name:Names.Id.t - -> udecl:UState.universe_decl - -> poly:bool - -> Proofview.telescope - -> t - -(** Update the proofs global environment after a side-effecting command - (e.g. a sublemma definition) has been run inside it. Assumes - there_are_pending_proofs. *) -val update_global_env : t -> t - -(* Takes a function to add to the exceptions data relative to the - state in which the proof was built *) -val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> proof_object - -(* Intermediate step necessary to delegate the future. - * Both access the current proof state. The former is supposed to be - * chained with a computation that completed the proof *) - -type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t - -(* If allow_partial is set (default no) then an incomplete proof - * is allowed (no error), and a warn is given if the proof is complete. *) -val return_proof : ?allow_partial:bool -> t -> closed_proof_output -val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t -> - closed_proof_output Future.computation -> proof_object - -val get_open_goals : t -> int - -val map_proof : (Proof.t -> Proof.t) -> t -> t -val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a -val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a - -(** Sets the tactic to be used when a tactic line is closed with [...] *) -val set_endline_tactic : Genarg.glob_generic_argument -> t -> t - -(** Sets the section variables assumed by the proof, returns its closure - * (w.r.t. type dependencies and let-ins covered by it) + a list of - * ids to be cleared *) -val set_used_variables : t -> - Names.Id.t list -> (Constr.named_context * Names.lident list) * t diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 0ce726db25..756fef0511 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -6,9 +6,7 @@ Proof Logic Goal_select Proof_bullet -Proof_global Refiner Tacmach -Pfedit Clenv Clenvtac diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 09d7e0278a..edeb27ab88 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -69,7 +69,7 @@ let rec shrink ctx sign c t accu = | _ -> assert false let shrink_entry sign const = - let open Proof_global in + let open Declare in let typ = match const.proof_entry_type with | None -> assert false | Some t -> t @@ -151,7 +151,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = in let const, args = shrink_entry sign const in let args = List.map EConstr.of_constr args in - let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in + let cd = Declare.DefinitionEntry { const with Declare.proof_entry_opaque = opaque } in let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in let cst () = (* do not compute the implicit arguments, it may be costly *) @@ -160,20 +160,20 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind cd in let cst, eff = Impargs.with_implicit_protection cst () in - let inst = match const.Proof_global.proof_entry_universes with + let inst = match const.Declare.proof_entry_universes with | Entries.Monomorphic_entry _ -> EInstance.empty | Entries.Polymorphic_entry (_, ctx) -> (* We mimic what the kernel does, that is ensuring that no additional constraints appear in the body of polymorphic constants. Ideally this should be enforced statically. *) - let (_, body_uctx), _ = Future.force const.Proof_global.proof_entry_body in + let (_, body_uctx), _ = Future.force const.Declare.proof_entry_body in let () = assert (Univ.ContextSet.is_empty body_uctx) in EInstance.make (Univ.UContext.instance ctx) in let lem = mkConstU (cst, inst) in let evd = Evd.set_universe_context evd ectx in let effs = Evd.concat_side_effects eff - Proof_global.(snd (Future.force const.proof_entry_body)) in + (snd (Future.force const.Declare.proof_entry_body)) in let solve = Proofview.tclEFFECTS effs <*> tacK lem args diff --git a/tactics/abstract.mli b/tactics/abstract.mli index e278729f89..96ddbea7b2 100644 --- a/tactics/abstract.mli +++ b/tactics/abstract.mli @@ -26,5 +26,5 @@ val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit P save path *) val shrink_entry : ('a, 'b) Context.Named.Declaration.pt list - -> 'c Proof_global.proof_entry - -> 'c Proof_global.proof_entry * Constr.t list + -> 'c Declare.proof_entry + -> 'c Declare.proof_entry * Constr.t list diff --git a/tactics/declare.ml b/tactics/declare.ml index c280760e84..694bd6d1cd 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -55,8 +55,20 @@ type constant_obj = { cst_locl : import_status; } +type 'a proof_entry = { + proof_entry_body : 'a Entries.const_entry_body; + (* List of section variables *) + proof_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + proof_entry_feedback : Stateid.t option; + proof_entry_type : Constr.types option; + proof_entry_universes : Entries.universes_entry; + proof_entry_opaque : bool; + proof_entry_inline_code : bool; +} + type 'a constant_entry = - | DefinitionEntry of 'a Proof_global.proof_entry + | DefinitionEntry of 'a proof_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry @@ -174,7 +186,6 @@ let record_aux env s_ty s_bo = let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body = - let open Proof_global in { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); proof_entry_secctx = None; proof_entry_type = types; @@ -184,7 +195,6 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types proof_entry_inline_code = inline} let cast_proof_entry e = - let open Proof_global in let (body, ctx), () = Future.force e.proof_entry_body in let univs = if Univ.ContextSet.is_empty ctx then e.proof_entry_universes @@ -205,7 +215,6 @@ let cast_proof_entry e = } let cast_opaque_proof_entry e = - let open Proof_global in let typ = match e.proof_entry_type with | None -> assert false | Some typ -> typ @@ -249,7 +258,6 @@ let is_unsafe_typing_flags () = not (flags.check_universes && flags.check_guarded && flags.check_positive) let define_constant ~side_effect ~name cd = - let open Proof_global in (* Logically define the constant and its subproofs, no libobject tampering *) let in_section = Lib.sections_are_opened () in let export, decl, unsafe = match cd with @@ -299,7 +307,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind (** Declaration of section variables and local definitions *) type variable_declaration = - | SectionLocalDef of Evd.side_effects Proof_global.proof_entry + | SectionLocalDef of Evd.side_effects proof_entry | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } (* This object is only for things which iterate over objects to find @@ -321,7 +329,6 @@ let declare_variable ~name ~kind d = | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) - let open Proof_global in let (body, eff) = Future.force de.proof_entry_body in let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in let eff = get_roles export eff in diff --git a/tactics/declare.mli b/tactics/declare.mli index 4ae9f6c7ae..4cb876cecb 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -19,14 +19,27 @@ open Entries reset works properly --- and will fill some global tables such as [Nametab] and [Impargs]. *) +(** Proof entries *) +type 'a proof_entry = { + proof_entry_body : 'a Entries.const_entry_body; + (* List of section variables *) + proof_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + proof_entry_feedback : Stateid.t option; + proof_entry_type : Constr.types option; + proof_entry_universes : Entries.universes_entry; + proof_entry_opaque : bool; + proof_entry_inline_code : bool; +} + (** Declaration of local constructions (Variable/Hypothesis/Local) *) type variable_declaration = - | SectionLocalDef of Evd.side_effects Proof_global.proof_entry + | SectionLocalDef of Evd.side_effects proof_entry | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } type 'a constant_entry = - | DefinitionEntry of 'a Proof_global.proof_entry + | DefinitionEntry of 'a proof_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry @@ -43,7 +56,7 @@ val declare_variable val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> ?univs:Entries.universes_entry -> - ?eff:Evd.side_effects -> constr -> Evd.side_effects Proof_global.proof_entry + ?eff:Evd.side_effects -> constr -> Evd.side_effects proof_entry type import_status = ImportDefaultBehavior | ImportNeedQualified diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index e2ef05461b..1f973ace6f 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -125,7 +125,7 @@ let define internal role id c poly univs = let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in let univs = UState.univ_entry ~poly ctx in let entry = { - Proof_global.proof_entry_body = + Declare.proof_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Evd.empty_side_effects); proof_entry_secctx = None; diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml new file mode 100644 index 0000000000..5be7b4fa28 --- /dev/null +++ b/tactics/pfedit.ml @@ -0,0 +1,195 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* !use_unification_heuristics_ref); + optwrite = (fun a -> use_unification_heuristics_ref:=a); +}) + +let use_unification_heuristics () = !use_unification_heuristics_ref + +exception NoSuchGoal +let () = CErrors.register_handler begin function + | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") + | _ -> raise CErrors.Unhandled +end + +let get_nth_V82_goal p i = + let Proof.{ sigma; goals } = Proof.data p in + try { it = List.nth goals (i-1) ; sigma } + with Failure _ -> raise NoSuchGoal + +let get_goal_context_gen pf i = + let { it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in + (sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) + +let get_goal_context pf i = + let p = Proof_global.get_proof pf in + get_goal_context_gen p i + +let get_current_goal_context pf = + let p = Proof_global.get_proof pf in + try get_goal_context_gen p 1 + with + | NoSuchGoal -> + (* spiwack: returning empty evar_map, since if there is no goal, + under focus, there is no accessible evar either. EJGA: this + seems strange, as we have pf *) + let env = Global.env () in + Evd.from_env env, env + +let get_current_context pf = + let p = Proof_global.get_proof pf in + try get_goal_context_gen p 1 + with + | NoSuchGoal -> + (* No more focused goals *) + let { Proof.sigma } = Proof.data p in + sigma, Global.env () + +let solve ?with_end_tac gi info_lvl tac pr = + let tac = match with_end_tac with + | None -> tac + | Some etac -> Proofview.tclTHEN tac etac in + let tac = match info_lvl with + | None -> tac + | Some _ -> Proofview.Trace.record_info_trace tac + in + let nosuchgoal = Proofview.tclZERO (Proof_bullet.SuggestNoSuchGoals (1,pr)) in + let tac = let open Goal_select in match gi with + | SelectAlreadyFocused -> + let open Proofview.Notations in + Proofview.numgoals >>= fun n -> + if n == 1 then tac + else + let e = CErrors.UserError + (None, + Pp.(str "Expected a single focused goal but " ++ + int n ++ str " goals are focused.")) + in + Proofview.tclZERO e + + | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac + | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac + | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac + | SelectAll -> tac + in + let tac = + if use_unification_heuristics () then + Proofview.tclTHEN tac Refine.solve_constraints + else tac + in + let env = Global.env () in + let (p,(status,info),()) = Proof.run_tactic env tac pr in + let env = Global.env () in + let sigma = Evd.from_env env in + let () = + match info_lvl with + | None -> () + | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info env sigma ~lvl:i info)) + in + (p,status) + +let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None tac) + +(**********************************************************************) +(* Shortcut to build a term using tactics *) + +let next = let n = ref 0 in fun () -> incr n; !n + +let build_constant_by_tactic ~name ctx sign ~poly typ tac = + let evd = Evd.from_ctx ctx in + let goals = [ (Global.env_of_context sign , typ) ] in + let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in + try + let pf, status = by tac pf in + let open Proof_global in + let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in + match entries with + | [entry] -> + let univs = UState.demote_seff_univs entry.Declare.proof_entry_universes universes in + entry, status, univs + | _ -> + CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") + with reraise -> + let reraise = CErrors.push reraise in + iraise reraise + +let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = + let name = Id.of_string ("temporary_proof"^string_of_int (next())) in + let sign = val_of_named_context (named_context env) in + let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in + let body, eff = Future.force ce.Declare.proof_entry_body in + let (cb, ctx) = + if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) + else body + in + let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in + cb, status, univs + +let refine_by_tactic ~name ~poly env sigma ty tac = + (* Save the initial side-effects to restore them afterwards. We set the + current set of side-effects to be empty so that we can retrieve the + ones created during the tactic invocation easily. *) + let eff = Evd.eval_side_effects sigma in + let sigma = Evd.drop_side_effects sigma in + (* Save the existing goals *) + let prev_future_goals = save_future_goals sigma in + (* Start a proof *) + let prf = Proof.start ~name ~poly sigma [env, ty] in + let (prf, _, ()) = + try Proof.run_tactic env tac prf + with Logic_monad.TacticFailure e as src -> + (* Catch the inner error of the monad tactic *) + let (_, info) = CErrors.push src in + iraise (e, info) + in + (* Plug back the retrieved sigma *) + let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in + assert (stack = []); + let ans = match Proofview.initial_goals entry with + | [c, _] -> c + | _ -> assert false + in + let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in + (* [neff] contains the freshly generated side-effects *) + let neff = Evd.eval_side_effects sigma in + (* Reset the old side-effects *) + let sigma = Evd.drop_side_effects sigma in + let sigma = Evd.emit_side_effects eff sigma in + (* Restore former goals *) + let sigma = restore_future_goals sigma prev_future_goals in + (* Push remaining goals as future_goals which is the only way we + have to inform the caller that there are goals to collect while + not being encapsulated in the monad *) + (* Goals produced by tactic "shelve" *) + let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in + (* Goals produced by tactic "give_up" *) + let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in + (* Other goals *) + let sigma = List.fold_right Evd.declare_future_goal goals sigma in + (* Get rid of the fresh side-effects by internalizing them in the term + itself. Note that this is unsound, because the tactic may have solved + other goals that were already present during its invocation, so that + those goals rely on effects that are not present anymore. Hopefully, + this hack will work in most cases. *) + let neff = neff.Evd.seff_private in + let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in + ans, sigma diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli new file mode 100644 index 0000000000..30514191fa --- /dev/null +++ b/tactics/pfedit.mli @@ -0,0 +1,89 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* int -> Evd.evar_map * env + +(** [get_current_goal_context ()] works as [get_goal_context 1] *) +val get_current_goal_context : Proof_global.t -> Evd.evar_map * env + +(** [get_current_context ()] returns the context of the + current focused goal. If there is no focused goal but there + is a proof in progress, it returns the corresponding evar_map. + If there is no pending proof then it returns the current global + environment and empty evar_map. *) +val get_current_context : Proof_global.t -> Evd.evar_map * env + +(** {6 ... } *) + +(** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th + subgoal of the current focused proof. [solve SelectAll + tac] applies [tac] to all subgoals. *) + +val solve : ?with_end_tac:unit Proofview.tactic -> + Goal_select.t -> int option -> unit Proofview.tactic -> + Proof.t -> Proof.t * bool + +(** [by tac] applies tactic [tac] to the 1st subgoal of the current + focused proof. + Returns [false] if an unsafe tactic has been used. *) + +val by : unit Proofview.tactic -> Proof_global.t -> Proof_global.t * bool + +(** Option telling if unification heuristics should be used. *) +val use_unification_heuristics : unit -> bool + +(** [build_by_tactic typ tac] returns a term of type [typ] by calling + [tac]. The return boolean, if [false] indicates the use of an unsafe + tactic. *) + +val build_constant_by_tactic + : name:Id.t + -> UState.t + -> named_context_val + -> poly:bool + -> EConstr.types + -> unit Proofview.tactic + -> Evd.side_effects Declare.proof_entry * bool * UState.t + +val build_by_tactic + : ?side_eff:bool + -> env + -> UState.t + -> poly:bool + -> EConstr.types + -> unit Proofview.tactic + -> constr * bool * UState.t + +val refine_by_tactic + : name:Id.t + -> poly:bool + -> env -> Evd.evar_map + -> EConstr.types + -> unit Proofview.tactic + -> constr * Evd.evar_map +(** A variant of the above function that handles open terms as well. + Caveat: all effects are purged in the returned term at the end, but other + evars solved by side-effects are NOT purged, so that unexpected failures may + occur. Ideally all code using this function should be rewritten in the + monad. *) diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml new file mode 100644 index 0000000000..a2929e45cd --- /dev/null +++ b/tactics/proof_global.ml @@ -0,0 +1,303 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* Proofview.tclUNIT () + | Some tac -> + let open Geninterp in + let {Proof.poly} = Proof.data ps.proof in + let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in + let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in + let tac = Geninterp.interp tag ist tac in + Ftactic.run tac (fun _ -> Proofview.tclUNIT ()) + in + let (newpr,ret) = f et ps.proof in + let ps = { ps with proof = newpr } in + ps, ret + +let compact_the_proof pf = map_proof Proof.compact pf + +(* Sets the tactic to be used when a tactic line is closed with [...] *) +let set_endline_tactic tac ps = + { ps with endline_tactic = Some tac } + +(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of + name [name] with goals [goals] (a list of pairs of environment and + conclusion). The proof is started in the evar map [sigma] (which + can typically contain universe constraints), and with universe + bindings [udecl]. *) +let start_proof ~name ~udecl ~poly sigma goals = + let proof = Proof.start ~name ~poly sigma goals in + let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in + { proof + ; endline_tactic = None + ; section_vars = None + ; udecl + ; initial_euctx + } + +let start_dependent_proof ~name ~udecl ~poly goals = + let proof = Proof.dependent_start ~name ~poly goals in + let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in + { proof + ; endline_tactic = None + ; section_vars = None + ; udecl + ; initial_euctx + } + +let get_used_variables pf = pf.section_vars +let get_universe_decl pf = pf.udecl + +let set_used_variables ps l = + let open Context.Named.Declaration in + let env = Global.env () in + let ids = List.fold_right Id.Set.add l Id.Set.empty in + let ctx = Environ.keep_hyps env ids in + let ctx_set = + List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in + let vars_of = Environ.global_vars_set in + let aux env entry (ctx, all_safe as orig) = + match entry with + | LocalAssum ({binder_name=x},_) -> + if Id.Set.mem x all_safe then orig + else (ctx, all_safe) + | LocalDef ({binder_name=x},bo, ty) as decl -> + if Id.Set.mem x all_safe then orig else + let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in + if Id.Set.subset vars all_safe + then (decl :: ctx, Id.Set.add x all_safe) + else (ctx, all_safe) in + let ctx, _ = + Environ.fold_named_context aux env ~init:(ctx,ctx_set) in + if not (Option.is_empty ps.section_vars) then + CErrors.user_err Pp.(str "Used section variables can be declared only once"); + (* EJGA: This is always empty thus we should modify the type *) + (ctx, []), { ps with section_vars = Some ctx} + +let get_open_goals ps = + let Proof.{ goals; stack; shelf } = Proof.data ps.proof in + List.length goals + + List.fold_left (+) 0 + (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + + List.length shelf + +type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t + +let private_poly_univs = + let b = ref true in + let _ = Goptions.(declare_bool_option { + optdepr = false; + optname = "use private polymorphic universes for Qed constants"; + optkey = ["Private";"Polymorphic";"Universes"]; + optread = (fun () -> !b); + optwrite = ((:=) b); + }) + in + fun () -> !b + +let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now + (fpl : closed_proof_output Future.computation) ps = + let { section_vars; proof; udecl; initial_euctx } = ps in + let Proof.{ name; poly; entry } = Proof.data proof in + let opaque = match opaque with Opaque -> true | Transparent -> false in + let constrain_variables ctx = + UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx + in + let fpl, univs = Future.split2 fpl in + let universes = if poly || now then Future.force univs else initial_euctx in + (* Because of dependent subgoals at the beginning of proofs, we could + have existential variables in the initial types of goals, we need to + normalise them for the kernel. *) + let subst_evar k = + let { Proof.sigma } = Proof.data proof in + Evd.existential_opt_value0 sigma k in + let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar + (UState.subst universes) in + + let make_body = + if poly || now then + let make_body t (c, eff) = + let body = c in + let allow_deferred = + not poly && (keep_body_ucst_separate || + not (Safe_typing.empty_private_constants = eff.Evd.seff_private)) + in + let typ = if allow_deferred then t else nf t in + let used_univs_body = Vars.universes_of_constr body in + let used_univs_typ = Vars.universes_of_constr typ in + if allow_deferred then + let initunivs = UState.univ_entry ~poly initial_euctx in + let ctx = constrain_variables universes in + (* For vi2vo compilation proofs are computed now but we need to + complement the univ constraints of the typ with the ones of + the body. So we keep the two sets distinct. *) + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let ctx_body = UState.restrict ctx used_univs in + let univs = UState.check_mono_univ_decl ctx_body udecl in + (initunivs, typ), ((body, univs), eff) + else if poly && opaque && private_poly_univs () then + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let universes = UState.restrict universes used_univs in + let typus = UState.restrict universes used_univs_typ in + let udecl = UState.check_univ_decl ~poly typus udecl in + let ubody = Univ.ContextSet.diff + (UState.context_set universes) + (UState.context_set typus) + in + (udecl, typ), ((body, ubody), eff) + else + (* Since the proof is computed now, we can simply have 1 set of + constraints in which we merge the ones for the body and the ones + for the typ. We recheck the declaration after restricting with + the actually used universes. + TODO: check if restrict is really necessary now. *) + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let ctx = UState.restrict universes used_univs in + let univs = UState.check_univ_decl ~poly ctx udecl in + (univs, typ), ((body, Univ.ContextSet.empty), eff) + in + fun t p -> Future.split2 (Future.chain p (make_body t)) + else + fun t p -> + (* Already checked the univ_decl for the type universes when starting the proof. *) + let univctx = UState.univ_entry ~poly:false universes in + let t = nf t in + Future.from_val (univctx, t), + Future.chain p (fun (pt,eff) -> + (* Deferred proof, we already checked the universe declaration with + the initial universes, ensure that the final universes respect + the declaration as well. If the declaration is non-extensible, + this will prevent the body from adding universes and constraints. *) + let univs = Future.force univs in + let univs = constrain_variables univs in + let used_univs = Univ.LSet.union + (Vars.universes_of_constr t) + (Vars.universes_of_constr pt) + in + let univs = UState.restrict univs used_univs in + let univs = UState.check_mono_univ_decl univs udecl in + (pt,univs),eff) + in + let entry_fn p (_, t) = + let t = EConstr.Unsafe.to_constr t in + let univstyp, body = make_body t p in + let univs, typ = Future.force univstyp in + let open Declare in + { + proof_entry_body = body; + proof_entry_secctx = section_vars; + proof_entry_feedback = feedback_id; + proof_entry_type = Some typ; + proof_entry_inline_code = false; + proof_entry_opaque = opaque; + proof_entry_universes = univs; } + in + let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in + { name; entries = entries; poly; universes; udecl } + +let return_proof ?(allow_partial=false) ps = + let { proof } = ps in + if allow_partial then begin + let proofs = Proof.partial_proof proof in + let Proof.{sigma=evd} = Proof.data proof in + let eff = Evd.eval_side_effects evd in + (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate + side-effects... This may explain why one need to uniquize side-effects + thereafter... *) + let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in + proofs, Evd.evar_universe_context evd + end else + let Proof.{name=pid;entry} = Proof.data proof in + let initial_goals = Proofview.initial_goals entry in + let evd = Proof.return ~pid proof in + let eff = Evd.eval_side_effects evd in + let evd = Evd.minimize_universes evd in + let proof_opt c = + match EConstr.to_constr_opt evd c with + | Some p -> p + | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain") + in + (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate + side-effects... This may explain why one need to uniquize side-effects + thereafter... *) + (* EJGA: actually side-effects de-duplication and this codepath is + unrelated. Duplicated side-effects arise from incorrect scheme + generation code, the main bulk of it was mostly fixed by #9836 + but duplication can still happen because of rewriting schemes I + think; however the code below is mostly untested, the only + code-paths that generate several proof entries are derive and + equations and so far there is no code in the CI that will + actually call those and do a side-effect, TTBOMK *) + let proofs = + List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in + proofs, Evd.evar_universe_context evd + +let close_future_proof ~opaque ~feedback_id ps proof = + close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps + +let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps = + close_proof ~opaque ~keep_body_ucst_separate ~now:true + (Future.from_val ~fix_exn (return_proof ps)) ps + +let update_global_env = + map_proof (fun p -> + let { Proof.sigma } = Proof.data p in + let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in + let p, (status,info), _ = Proof.run_tactic (Global.env ()) tac p in + p) diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli new file mode 100644 index 0000000000..d15e23c2cc --- /dev/null +++ b/tactics/proof_global.mli @@ -0,0 +1,103 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* Proof.t +val get_proof_name : t -> Names.Id.t +val get_used_variables : t -> Constr.named_context option + +(** Get the universe declaration associated to the current proof. *) +val get_universe_decl : t -> UState.universe_decl + +(** Get initial universe state *) +val get_initial_euctx : t -> UState.t + +val compact_the_proof : t -> t + +(** When a proof is closed, it is reified into a [proof_object] *) +type proof_object = + { name : Names.Id.t + (** name of the proof *) + ; entries : Evd.side_effects Declare.proof_entry list + (** list of the proof terms (in a form suitable for definitions). *) + ; poly : bool + (** polymorphic status *) + ; universes: UState.t + (** universe state *) + ; udecl : UState.universe_decl + (** universe declaration *) + } + +type opacity_flag = Opaque | Transparent + +(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of + name [name] with goals [goals] (a list of pairs of environment and + conclusion); [poly] determines if the proof is universe + polymorphic. The proof is started in the evar map [sigma] (which + can typically contain universe constraints), and with universe + bindings [udecl]. *) +val start_proof + : name:Names.Id.t + -> udecl:UState.universe_decl + -> poly:bool + -> Evd.evar_map + -> (Environ.env * EConstr.types) list + -> t + +(** Like [start_proof] except that there may be dependencies between + initial goals. *) +val start_dependent_proof + : name:Names.Id.t + -> udecl:UState.universe_decl + -> poly:bool + -> Proofview.telescope + -> t + +(** Update the proofs global environment after a side-effecting command + (e.g. a sublemma definition) has been run inside it. Assumes + there_are_pending_proofs. *) +val update_global_env : t -> t + +(* Takes a function to add to the exceptions data relative to the + state in which the proof was built *) +val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> proof_object + +(* Intermediate step necessary to delegate the future. + * Both access the current proof state. The former is supposed to be + * chained with a computation that completed the proof *) + +type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t + +(* If allow_partial is set (default no) then an incomplete proof + * is allowed (no error), and a warn is given if the proof is complete. *) +val return_proof : ?allow_partial:bool -> t -> closed_proof_output +val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t -> + closed_proof_output Future.computation -> proof_object + +val get_open_goals : t -> int + +val map_proof : (Proof.t -> Proof.t) -> t -> t +val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a +val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a + +(** Sets the tactic to be used when a tactic line is closed with [...] *) +val set_endline_tactic : Genarg.glob_generic_argument -> t -> t + +(** Sets the section variables assumed by the proof, returns its closure + * (w.r.t. type dependencies and let-ins covered by it) + a list of + * ids to be cleared *) +val set_used_variables : t -> + Names.Id.t list -> (Constr.named_context * Names.lident list) * t diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 6dd749aa0d..c5c7969a09 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,4 +1,6 @@ Declare +Proof_global +Pfedit Dnet Dn Btermdn diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 57de719cb4..9745358ba2 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -85,12 +85,12 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o in if program_mode then let env = Global.env () in - let (c,ctx), sideff = Future.force ce.Proof_global.proof_entry_body in + let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); assert(Univ.ContextSet.is_empty ctx); Obligations.check_evars env evd; let c = EConstr.of_constr c in - let typ = match ce.Proof_global.proof_entry_type with + let typ = match ce.Declare.proof_entry_type with | Some t -> EConstr.of_constr t | None -> Retyping.get_type_of env evd c in diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index db0c102e14..01505d0733 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -41,5 +41,5 @@ val interp_definition -> red_expr option -> constr_expr -> constr_expr option - -> Evd.side_effects Proof_global.proof_entry * + -> Evd.side_effects Declare.proof_entry * Evd.evar_map * UState.universe_decl * Impargs.manual_implicits diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 5e4f2dcd34..1926faaf0e 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -44,7 +44,7 @@ end (* Locality stuff *) let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = - let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in + let fix_exn = Future.fix_exn_of ce.proof_entry_body in let gr = match scope with | Discharge -> let () = diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 606cfade46..54a0c9a7e8 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -45,7 +45,7 @@ val declare_definition -> kind:Decls.definition_object_kind -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) -> UnivNames.universe_binders - -> Evd.side_effects Proof_global.proof_entry + -> Evd.side_effects Declare.proof_entry -> Impargs.manual_implicits -> GlobRef.t @@ -66,7 +66,7 @@ val prepare_definition : allow_evars:bool -> ?opaque:bool -> ?inline:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> types:EConstr.t option -> body:EConstr.t -> - Evd.evar_map * Evd.side_effects Proof_global.proof_entry + Evd.evar_map * Evd.side_effects Declare.proof_entry val prepare_parameter : allow_evars:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types -> diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index c5cbb095ca..9c8213ad8a 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -153,7 +153,7 @@ let declare_obligation prg obl body ty uctx = ((body, Univ.ContextSet.empty), Evd.empty_side_effects) in let ce = - Proof_global.{ proof_entry_body = Future.from_val ~fix_exn:(fun x -> x) body + { Declare.proof_entry_body = Future.from_val ~fix_exn:(fun x -> x) body ; proof_entry_secctx = None ; proof_entry_type = ty ; proof_entry_universes = uctx @@ -495,12 +495,11 @@ type obligation_qed_info = } let obligation_terminator entries uctx { name; num; auto } = - let open Proof_global in match entries with | [entry] -> let env = Global.env () in - let ty = entry.proof_entry_type in - let body, eff = Future.force entry.proof_entry_body in + let ty = entry.Declare.proof_entry_type in + let body, eff = Future.force entry.Declare.proof_entry_body in let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in let sigma = Evd.from_ctx uctx in let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in @@ -514,7 +513,7 @@ let obligation_terminator entries uctx { name; num; auto } = let obls, rem = prg.prg_obligations in let obl = obls.(num) in let status = - match obl.obl_status, entry.proof_entry_opaque with + match obl.obl_status, entry.Declare.proof_entry_opaque with | (_, Evar_kinds.Expand), true -> err_not_transp () | (true, _), true -> err_not_transp () | (false, _), true -> Evar_kinds.Define true diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index 2a8fa734b3..7d8a112cc6 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -76,7 +76,7 @@ type obligation_qed_info = } val obligation_terminator - : Evd.side_effects Proof_global.proof_entry list + : Evd.side_effects Declare.proof_entry list -> UState.t -> obligation_qed_info -> unit (** [obligation_terminator] part 2 of saving an obligation *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index cf87646905..18955c2ba3 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -101,7 +101,6 @@ let () = let define ~poly name sigma c t = let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in let univs = Evd.univ_entry ~poly sigma in - let open Proof_global in let kn = f ~name (DefinitionEntry { proof_entry_body = c; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 7809425a10..42d1a1f3fc 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -383,10 +383,9 @@ let adjust_guardness_conditions const = function | possible_indexes -> (* Try all combinations... not optimal *) let env = Global.env() in - let open Proof_global in { const with - proof_entry_body = - Future.chain const.proof_entry_body + Declare.proof_entry_body = + Future.chain const.Declare.proof_entry_body (fun ((body, ctx), eff) -> match Constr.kind body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> @@ -404,10 +403,11 @@ let finish_proved env sigma idopt po info = let name = match idopt with | None -> name | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in - let fix_exn = Future.fix_exn_of const.proof_entry_body in + let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in let () = try let const = adjust_guardness_conditions const compute_guard in - let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in + let should_suggest = const.Declare.proof_entry_opaque && + Option.is_empty const.Declare.proof_entry_secctx in let open DeclareDef in let r = match scope with | Discharge -> @@ -451,7 +451,7 @@ let finish_derived ~f ~name ~idopt ~entries = in (* The opacity of [f_def] is adjusted to be [false], as it must. Then [f] is declared in the global environment. *) - let f_def = { f_def with Proof_global.proof_entry_opaque = false } in + let f_def = { f_def with Declare.proof_entry_opaque = false } in let f_kind = Decls.(IsDefinition Definition) in let f_def = Declare.DefinitionEntry f_def in let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in @@ -463,17 +463,17 @@ let finish_derived ~f ~name ~idopt ~entries = let substf c = Vars.replace_vars [f,f_kn_term] c in (* Extracts the type of the proof of [suchthat]. *) let lemma_pretype = - match Proof_global.(lemma_def.proof_entry_type) with + match lemma_def.Declare.proof_entry_type with | Some t -> t | None -> assert false (* Proof_global always sets type here. *) in (* The references of [f] are subsituted appropriately. *) let lemma_type = substf lemma_pretype in (* The same is done in the body of the proof. *) - let lemma_body = Future.chain Proof_global.(lemma_def.proof_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in - let lemma_def = let open Proof_global in + let lemma_body = Future.chain lemma_def.Declare.proof_entry_body (fun ((b,ctx),fx) -> (substf b, ctx), fx) in + let lemma_def = { lemma_def with - proof_entry_body = lemma_body; + Declare.proof_entry_body = lemma_body; proof_entry_type = Some lemma_type } in let lemma_def = Declare.DefinitionEntry lemma_def in @@ -530,7 +530,7 @@ let save_lemma_admitted_delayed ~proof ~info = let { Info.hook; scope; impargs; other_thms } = info in if List.length entries <> 1 then user_err Pp.(str "Admitted does not support multiple statements"); - let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in + let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in let poly = match proof_entry_universes with | Entries.Monomorphic_entry _ -> false | Entries.Polymorphic_entry (_, _) -> true in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 37fe0df0ee..5d153fa8be 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -423,11 +423,11 @@ let solve_by_tac ?loc name evi t poly ctx = Pfedit.build_constant_by_tactic ~name ~poly ctx evi.evar_hyps evi.evar_concl t in let env = Global.env () in - let (body, eff) = Future.force entry.Proof_global.proof_entry_body in + let (body, eff) = Future.force entry.Declare.proof_entry_body in let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); - Some (fst body, entry.Proof_global.proof_entry_type, Evd.evar_universe_context ctx') + Some (fst body, entry.Declare.proof_entry_type, Evd.evar_universe_context ctx') with | Refiner.FailError (_, s) as exn -> let _ = CErrors.push exn in diff --git a/vernac/record.ml b/vernac/record.ml index 86745212e7..1bb8ddf5dc 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -340,7 +340,6 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in try - let open Proof_global in let entry = { proof_entry_body = Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects); -- cgit v1.2.3