diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 6 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 11 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 32 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 15 |
4 files changed, 35 insertions, 29 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 1937885587..23f96b5a32 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -239,7 +239,6 @@ let get_current_proof_name = Proof_global.get_current_proof_name let get_all_proof_names = Proof_global.get_all_proof_names type lemma_possible_guards = Proof_global.lemma_possible_guards -type universe_binders = Proof_global.universe_binders let delete_proof = Proof_global.discard let delete_current_proof = Proof_global.discard_current @@ -257,6 +256,5 @@ let set_used_variables l = let get_used_variables () = Proof_global.get_used_variables () -let get_universe_binders () = - Proof_global.get_universe_binders () - +let get_universe_decl () = + Proof_global.get_universe_decl () diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 745ee8f367..6e4ecd13b3 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -23,7 +23,7 @@ open Decl_kinds proof of mutually dependent theorems) *) val start_proof : - Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr -> + Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr -> ?init_tac:unit Proofview.tactic -> Proof_global.proof_terminator -> unit @@ -67,6 +67,7 @@ val current_proof_statement : unit -> Id.t * goal_kind * EConstr.types (** {6 ... } *) + (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th subgoal of the current focused proof or raises a [UserError] if no proof is focused or if there is no [n]th subgoal. [solve SelectAll @@ -185,8 +186,8 @@ val get_used_variables : unit -> Context.Named.t option [@@ocaml.deprecated "use Proof_global.get_used_variables"] (** {6 Universe binders } *) -val get_universe_binders : unit -> Proof_global.universe_binders option -[@@ocaml.deprecated "use Proof_global.get_universe_binders"] +val get_universe_decl : unit -> Univdecls.universe_decl +[@@ocaml.deprecated "use Proof_global.get_universe_decl"] (** {6 ... } *) (** [get_current_proof_name ()] return the name of the current focused @@ -202,7 +203,3 @@ val get_all_proof_names : unit -> Id.t list type lemma_possible_guards = Proof_global.lemma_possible_guards [@@ocaml.deprecated "use Proof_global.lemma_possible_guards"] - -type universe_binders = Proof_global.universe_binders -[@@ocaml.deprecated "use Proof_global.universe_binders"] - diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 2ade797f63..e8266f5c86 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -69,7 +69,6 @@ let _ = (* Extra info on proofs. *) type lemma_possible_guards = int list list type proof_universes = Evd.evar_universe_context * Universes.universe_binders option -type universe_binders = Id.t Loc.located list type proof_object = { id : Names.Id.t; @@ -94,7 +93,7 @@ type pstate = { proof : Proof.proof; strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; - universe_binders: universe_binders option; + universe_decl: Univdecls.universe_decl; } let make_terminator f = f @@ -230,15 +229,22 @@ let activate_proof_mode mode = let disactivate_current_proof_mode () = CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()) -(** [start_proof sigma id str goals terminator] starts a proof of name +let default_universe_decl = + let open Misctypes in + { univdecl_instance = []; + univdecl_extensible_instance = true; + univdecl_constraints = Univ.Constraint.empty; + univdecl_extensible_constraints = true } + +(** [start_proof sigma id pl str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this is (spiwack: for potential printing, I believe is used only by closing commands and the xml plugin); [terminator] is used at the end of the proof to close the proof. The proof is started in the evar map [sigma] (which can typically contain universe - constraints). *) -let start_proof sigma id ?pl str goals terminator = + constraints), and with universe bindings pl. *) +let start_proof sigma id ?(pl=default_universe_decl) str goals terminator = let initial_state = { pid = id; terminator = CEphemeron.create terminator; @@ -247,10 +253,10 @@ let start_proof sigma id ?pl str goals terminator = section_vars = None; strength = str; mode = find_proof_mode "No"; - universe_binders = pl } in + universe_decl = pl } in push initial_state pstates -let start_dependent_proof id ?pl str goals terminator = +let start_dependent_proof id ?(pl=default_universe_decl) str goals terminator = let initial_state = { pid = id; terminator = CEphemeron.create terminator; @@ -259,11 +265,11 @@ let start_dependent_proof id ?pl str goals terminator = section_vars = None; strength = str; mode = find_proof_mode "No"; - universe_binders = pl } in + universe_decl = pl } in push initial_state pstates let get_used_variables () = (cur_pstate ()).section_vars -let get_universe_binders () = (cur_pstate ()).universe_binders +let get_universe_decl () = (cur_pstate ()).universe_decl let proof_using_auto_clear = ref false let _ = Goptions.declare_bool_option @@ -319,7 +325,7 @@ type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * let close_proof ~keep_body_ucst_separate ?feedback_id ~now (fpl : closed_proof_output Future.computation) = - let { pid; section_vars; strength; proof; terminator; universe_binders } = + let { pid; section_vars; strength; proof; terminator; universe_decl } = cur_pstate () in let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in @@ -393,8 +399,10 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now }) fpl initial_goals in let binders = - Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes))) - universe_binders + if not poly || (List.is_empty universe_decl.Misctypes.univdecl_instance && + universe_decl.Misctypes.univdecl_extensible_instance) then None + else + Some (fst (Evd.check_univ_decl (Evd.from_ctx universes) universe_decl)) in { id = pid; entries = entries; persistence = strength; universes = (universes, binders) }, diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 52f5f74046..8c0f6ad85f 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -34,7 +34,7 @@ val compact_the_proof : unit -> unit values. *) type lemma_possible_guards = int list list type proof_universes = Evd.evar_universe_context * Universes.universe_binders option -type universe_binders = Names.Id.t Loc.located list + type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; @@ -54,21 +54,23 @@ type closed_proof = proof_object * proof_terminator val make_terminator : (proof_ending -> unit) -> proof_terminator val apply_terminator : proof_terminator -> proof_ending -> unit -(** [start_proof id str goals terminator] starts a proof of name [id] +(** [start_proof id str pl goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this is (spiwack: for potential printing, I believe is used only by closing commands and the xml plugin); [terminator] is used at the - end of the proof to close the proof. *) + end of the proof to close the proof. The proof is started in the + evar map [sigma] (which can typically contain universe + constraints), and with universe bindings pl. *) val start_proof : - Evd.evar_map -> Names.Id.t -> ?pl:universe_binders -> + Evd.evar_map -> Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list -> proof_terminator -> unit (** Like [start_proof] except that there may be dependencies between initial goals. *) val start_dependent_proof : - Names.Id.t -> ?pl:universe_binders -> Decl_kinds.goal_kind -> + Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> Proofview.telescope -> proof_terminator -> unit (** Update the proofs global environment after a side-effecting command @@ -119,7 +121,8 @@ val set_used_variables : Names.Id.t list -> Context.Named.t * Names.Id.t Loc.located list val get_used_variables : unit -> Context.Named.t option -val get_universe_binders : unit -> universe_binders option +(** Get the universe declaration associated to the current proof. *) +val get_universe_decl : unit -> Univdecls.universe_decl module V82 : sig val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list * |