diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal_select.ml | 2 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 18 | ||||
| -rw-r--r-- | proofs/proof_bullet.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 55 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 4 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 14 |
6 files changed, 59 insertions, 36 deletions
diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml index 65a94a2c60..cef3fd3f5e 100644 --- a/proofs/goal_select.ml +++ b/proofs/goal_select.ml @@ -53,7 +53,7 @@ let parse_goal_selector = function with Failure _ -> CErrors.user_err Pp.(str err_msg) end -let _ = let open Goptions in +let () = let open Goptions in declare_string_option { optdepr = false; optname = "default goal selector" ; diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 81122e6858..886a62cb89 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -16,18 +16,18 @@ open Environ open Evd let use_unification_heuristics_ref = ref true -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "Solve unification constraints at every \".\""; - Goptions.optkey = ["Solve";"Unification";"Constraints"]; - Goptions.optread = (fun () -> !use_unification_heuristics_ref); - Goptions.optwrite = (fun a -> use_unification_heuristics_ref:=a); -} +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Solve unification constraints at every \".\""; + optkey = ["Solve";"Unification";"Constraints"]; + optread = (fun () -> !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 +let () = CErrors.register_handler begin function | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") | _ -> raise CErrors.Unhandled end @@ -138,7 +138,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo try let status = by tac in let open Proof_global in - let { entries; universes } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in + let { entries; universes } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) in match entries with | [entry] -> discard_current (); diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index ed8df29d7b..2ca4f0afb4 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -176,7 +176,7 @@ end (* Current bullet behavior, controlled by the option *) let current_behavior = ref Strict.strict -let _ = +let () = Goptions.(declare_string_option { optdepr = false; optname = "bullet behavior"; diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index cb4b5759dc..095aa36f03 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -53,7 +53,7 @@ let default_proof_mode = ref (find_proof_mode "No") let get_default_proof_mode_name () = (CEphemeron.default !default_proof_mode standard).name -let _ = +let () = Goptions.(declare_string_option { optdepr = false; optname = "default proof mode" ; @@ -128,13 +128,13 @@ let push a l = l := a::!l; update_proof_mode () exception NoSuchProof -let _ = CErrors.register_handler begin function +let () = CErrors.register_handler begin function | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.") | _ -> raise CErrors.Unhandled end exception NoCurrentProof -let _ = CErrors.register_handler begin function +let () = CErrors.register_handler begin function | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") | _ -> raise CErrors.Unhandled end @@ -272,12 +272,12 @@ let get_used_variables () = (cur_pstate ()).section_vars let get_universe_decl () = (cur_pstate ()).universe_decl let proof_using_auto_clear = ref false -let _ = Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = "Proof using Clear Unused"; - Goptions.optkey = ["Proof";"Using";"Clear";"Unused"]; - Goptions.optread = (fun () -> !proof_using_auto_clear); - Goptions.optwrite = (fun b -> proof_using_auto_clear := b) } +let () = Goptions.(declare_bool_option + { optdepr = false; + optname = "Proof using Clear Unused"; + optkey = ["Proof";"Using";"Clear";"Unused"]; + optread = (fun () -> !proof_using_auto_clear); + optwrite = (fun b -> proof_using_auto_clear := b) }) let set_used_variables l = let open Context.Named.Declaration in @@ -318,10 +318,23 @@ let get_open_goals () = type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t -let close_proof ~keep_body_ucst_separate ?feedback_id ~now +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) = let { pid; section_vars; strength; proof; terminator; universe_decl } = cur_pstate () in + let opaque = match opaque with Opaque -> true | Transparent -> false in let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in let initial_euctx = Proof.initial_euctx proof in @@ -358,6 +371,16 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let ctx_body = UState.restrict ctx used_univs in let univs = UState.check_mono_univ_decl ctx_body universe_decl 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 universe_decl 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 @@ -394,7 +417,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now const_entry_feedback = feedback_id; const_entry_type = Some typ; const_entry_inline_code = false; - const_entry_opaque = true; + const_entry_opaque = opaque; const_entry_universes = univs; } in let entries = Future.map2 entry_fn fpl initial_goals in @@ -425,10 +448,10 @@ let return_proof ?(allow_partial=false) () = List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in proofs, Evd.evar_universe_context evd -let close_future_proof ~feedback_id proof = - close_proof ~keep_body_ucst_separate:true ~feedback_id ~now:false proof -let close_proof ~keep_body_ucst_separate fix_exn = - close_proof ~keep_body_ucst_separate ~now:true +let close_future_proof ~opaque ~feedback_id proof = + close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof +let close_proof ~opaque ~keep_body_ucst_separate fix_exn = + close_proof ~opaque ~keep_body_ucst_separate ~now:true (Future.from_val ~fix_exn (return_proof ())) (** Gets the current terminator without checking that the proof has @@ -467,7 +490,7 @@ let update_global_env () = (p, ()))) (* XXX: Bullet hook, should be really moved elsewhere *) -let _ = +let () = let hook n = try let prf = give_me_the_proof () in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index e3808bc36d..d9c32cf9d5 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -86,7 +86,7 @@ val update_global_env : unit -> unit (* Takes a function to add to the exceptions data relative to the state in which the proof was built *) -val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof +val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof (* Intermediate step necessary to delegate the future. * Both access the current proof state. The former is supposed to be @@ -97,7 +97,7 @@ type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * USt (* 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 -> unit -> closed_proof_output -val close_future_proof : feedback_id:Stateid.t -> +val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> closed_proof_output Future.computation -> closed_proof (** Gets the current terminator without checking that the proof has diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 0981584bb5..6658c37f41 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -54,14 +54,14 @@ let strong_cbn flags = strong_with_flags whd_cbn flags let simplIsCbn = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Plug the simpl tactic to the new cbn mechanism"; - Goptions.optkey = ["SimplIsCbn"]; - Goptions.optread = (fun () -> !simplIsCbn); - Goptions.optwrite = (fun a -> simplIsCbn:=a); -} + optkey = ["SimplIsCbn"]; + optread = (fun () -> !simplIsCbn); + optwrite = (fun a -> simplIsCbn:=a); +}) let set_strategy_one ref l = let k = |