diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.mli | 3 | ||||
| -rw-r--r-- | proofs/proof.ml | 36 | ||||
| -rw-r--r-- | proofs/proof.mli | 3 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 7 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 4 |
5 files changed, 47 insertions, 6 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 7b79732249..e02b5ab956 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -85,6 +85,9 @@ val solve : ?with_end_tac:unit Proofview.tactic -> val by : unit Proofview.tactic -> bool +(** Option telling if unification heuristics should be used. *) +val use_unification_heuristics : unit -> bool + (** [instantiate_nth_evar_com n c] instantiate the [n]th undefined existential variable of the current focused proof by [c] or raises a UserError if no proof is focused or if there is no such [n]th diff --git a/proofs/proof.ml b/proofs/proof.ml index 51e0a1d614..0d355890c5 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -63,6 +63,7 @@ exception CannotUnfocusThisWay (* Cannot focus on non-existing subgoals *) exception NoSuchGoals of int * int +exception NoSuchGoal of Names.Id.t exception FullyUnfocused @@ -75,6 +76,10 @@ let _ = CErrors.register_handler begin function CErrors.user_err ~hdr:"Focus" Pp.( str"Not every goal in range ["++ int i ++ str","++int j++str"] exist." ) + | NoSuchGoal id -> + CErrors.user_err + ~hdr:"Focus" + Pp.(str "No such goal: " ++ str (Names.Id.to_string id) ++ str ".") | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused") | _ -> raise CErrors.Unhandled end @@ -230,6 +235,37 @@ let focus cond inf i pr = try _focus cond (Obj.repr inf) i i pr with CList.IndexOutOfRange -> raise (NoSuchGoals (i,i)) +(* Focus on the goal named id *) +let focus_id cond inf id pr = + let (focused_goals, evar_map) = Proofview.proofview pr.proofview in + begin match try Some (Evd.evar_key id evar_map) with Not_found -> None with + | Some ev -> + begin match CList.safe_index Evar.equal ev focused_goals with + | Some i -> + (* goal is already under focus *) + _focus cond (Obj.repr inf) i i pr + | None -> + if CList.mem_f Evar.equal ev pr.shelf then + (* goal is on the shelf, put it in focus *) + let proofview = Proofview.unshelve [ev] pr.proofview in + let shelf = + CList.filter (fun ev' -> Evar.equal ev ev' |> not) pr.shelf + in + let pr = { pr with proofview; shelf } in + let (focused_goals, _) = Proofview.proofview pr.proofview in + let i = + (* Now we know that this will succeed *) + try CList.index Evar.equal ev focused_goals + with Not_found -> assert false + in + _focus cond (Obj.repr inf) i i pr + else + raise CannotUnfocusThisWay + end + | None -> + raise (NoSuchGoal id) + end + let rec unfocus kind pr () = let cond = cond_of_focus pr in match test_cond cond kind pr.proofview with diff --git a/proofs/proof.mli b/proofs/proof.mli index c0e832fb8c..33addf13d7 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -137,6 +137,9 @@ val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition a need for it? *) val focus : 'a focus_condition -> 'a -> int -> t -> t +(* focus on goal named id *) +val focus_id : 'aa focus_condition -> 'a -> Names.Id.t -> t -> t + exception FullyUnfocused exception CannotUnfocusThisWay diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 3120c97b58..7e250faa86 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -93,7 +93,7 @@ type pstate = { pid : Id.t; (* the name of the theorem whose proof is being constructed *) terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; - section_vars : Context.Named.t option; + section_vars : Constr.named_context option; proof : Proof.t; strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; @@ -348,9 +348,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now not (Safe_typing.empty_private_constants = eff)) in let typ = if allow_deferred then t else nf t in - let env = Global.env () in - let used_univs_body = Univops.universes_of_constr env body in - let used_univs_typ = Univops.universes_of_constr env typ in + let used_univs_body = Univops.universes_of_constr body in + let used_univs_typ = Univops.universes_of_constr typ in if allow_deferred then let initunivs = UState.const_univ_entry ~poly initial_euctx in let ctx = constrain_variables universes in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 9e07ed2d05..854ceaa41a 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -126,8 +126,8 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit * (w.r.t. type dependencies and let-ins covered by it) + a list of * ids to be cleared *) val set_used_variables : - Names.Id.t list -> Context.Named.t * Names.lident list -val get_used_variables : unit -> Context.Named.t option + Names.Id.t list -> Constr.named_context * Names.lident list +val get_used_variables : unit -> Constr.named_context option (** Get the universe declaration associated to the current proof. *) val get_universe_decl : unit -> UState.universe_decl |