diff options
| -rw-r--r-- | stm/stm.ml | 14 | ||||
| -rw-r--r-- | tactics/proof_global.ml | 13 | ||||
| -rw-r--r-- | tactics/proof_global.mli | 3 | ||||
| -rw-r--r-- | vernac/vernacstate.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacstate.mli | 1 |
5 files changed, 17 insertions, 18 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index c1156b9afe..5b88ee3d68 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1522,15 +1522,15 @@ end = struct (* {{{ *) let st = State.freeze () in if not drop then begin let checked_proof = Future.chain future_proof (fun p -> - let opaque = Proof_global.Opaque in (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) State.unfreeze st; let pobject, _info = - PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in + PG_compat.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in let st = Vernacstate.freeze_interp_state ~marshallable:false in + let opaque = Proof_global.Opaque in stm_qed_delay_proof ~st ~id:stop ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))) in ignore(Future.join checked_proof); @@ -2479,13 +2479,13 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = ~drop_pt exn_info block_stop, ref false in qed.fproof <- Some (Some fp, cancel); - let opaque = match keep' with - | VtKeepAxiom | VtKeepOpaque -> - Proof_global.Opaque (* Admitted -> Opaque should be OK. *) - | VtKeepDefined -> Proof_global.Transparent + let () = match keep' with + | VtKeepAxiom | VtKeepOpaque -> () + | VtKeepDefined -> + CErrors.anomaly (Pp.str "Cannot delegate transparent proofs, this is a bug in the STM.") in let proof, info = - PG_compat.close_future_proof ~opaque ~feedback_id:id fp in + PG_compat.close_future_proof ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; let st = Vernacstate.freeze_interp_state ~marshallable:false in diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index 7d86c6a1d1..d7f4cb3b9a 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -226,7 +226,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps = let entries = CList.map2 make_entry elist (Proofview.initial_goals entry) in { name; entries; uctx } -let close_proof_delayed ~opaque ?feedback_id (fpl : closed_proof_output Future.computation) ps = +let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) = let { section_vars; proof; udecl; initial_euctx } = ps in let { Proof.name; poly; entry; sigma } = Proof.data proof in @@ -234,7 +234,6 @@ let close_proof_delayed ~opaque ?feedback_id (fpl : closed_proof_output Future.c if poly then CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants."); - let opaque = match opaque with Opaque -> true | Transparent -> false in let fpl, uctx = Future.split2 fpl in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to @@ -242,6 +241,9 @@ let close_proof_delayed ~opaque ?feedback_id (fpl : closed_proof_output Future.c let subst_evar k = Evd.existential_opt_value0 sigma k in let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst initial_euctx) in + (* We only support opaque proofs, this will be enforced by using + different entries soon *) + let opaque = true in let make_entry p (_, types) = (* Already checked the univ_decl for the type universes when starting the proof. *) let univs = UState.univ_entry ~poly:false initial_euctx in @@ -261,11 +263,13 @@ let close_proof_delayed ~opaque ?feedback_id (fpl : closed_proof_output Future.c let univs = UState.restrict uctx used_univs in let univs = UState.check_mono_univ_decl univs udecl in (pt,univs),eff) - |> Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types + |> Declare.delayed_definition_entry ~opaque ~feedback_id ?section_vars ~univs ~types in let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in { name; entries; uctx = initial_euctx } +let close_future_proof = close_proof_delayed + let return_partial_proof { proof } = let proofs = Proof.partial_proof proof in let Proof.{sigma=evd} = Proof.data proof in @@ -276,9 +280,6 @@ let return_partial_proof { proof } = let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in proofs, Evd.evar_universe_context evd -let close_future_proof ~opaque ~feedback_id ps proof = - close_proof_delayed ~opaque ~feedback_id proof ps - let update_global_env = map_proof (fun p -> let { Proof.sigma } = Proof.data p in diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli index 59881dffa1..874708ded8 100644 --- a/tactics/proof_global.mli +++ b/tactics/proof_global.mli @@ -81,8 +81,7 @@ val return_proof : t -> closed_proof_output (** An incomplete proof is allowed (no error), and a warn is given if the proof is complete. *) val return_partial_proof : t -> closed_proof_output -val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t -> - closed_proof_output Future.computation -> proof_object +val close_future_proof : feedback_id:Stateid.t -> t -> closed_proof_output Future.computation -> proof_object val get_open_goals : t -> int diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index b722acd1ad..a4e9c8e1ab 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -167,8 +167,8 @@ module Proof_global = struct let return_proof () = cc return_proof let return_partial_proof () = cc return_partial_proof - let close_future_proof ~opaque ~feedback_id pf = - cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt, + let close_future_proof ~feedback_id pf = + cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~feedback_id st pf) pt, Internal.get_info pt) let close_proof ~opaque ~keep_body_ucst_separate = diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index b6b24c9275..9c4de7720c 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -71,7 +71,6 @@ module Proof_global : sig type closed_proof = Proof_global.proof_object * Lemmas.Info.t val close_future_proof : - opaque:Proof_global.opacity_flag -> feedback_id:Stateid.t -> Proof_global.closed_proof_output Future.computation -> closed_proof |