diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 4 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 5 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 5 | ||||
| -rw-r--r-- | proofs/proof.ml | 6 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 16 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 8 | ||||
| -rw-r--r-- | proofs/refine.ml | 20 | ||||
| -rw-r--r-- | proofs/refine.mli | 11 |
9 files changed, 10 insertions, 67 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 1f1bdf4da7..9540d3de44 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -677,7 +677,7 @@ let define_with_type sigma env ev c = let t = Retyping.get_type_of env sigma ev in let ty = Retyping.get_type_of env sigma c in let j = Environ.make_judge c ty in - let (sigma, j) = Coercion.inh_conv_coerce_to true env sigma j t in + let (sigma, j) = Coercion.inh_conv_coerce_to ~program_mode:false true env sigma j t in let (ev, _) = destEvar sigma ev in let sigma = Evd.define ev j.Environ.uj_val sigma in sigma diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 6c4193c66b..1b2756f49f 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -53,7 +53,9 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = true; Pretyping.fail_evar = false; - Pretyping.expand_evars = true } in + Pretyping.expand_evars = true; + Pretyping.program_mode = false; + } in try Pretyping.understand_ltac flags env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc with e when CErrors.noncritical e -> diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 7f1ae6d12b..9509c36ec0 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -70,11 +70,6 @@ let get_current_context ?p () = let evd = Proof.in_proof p (fun x -> x) in (evd, Global.env ()) -let current_proof_statement () = - match Proof_global.V82.get_current_initial_conclusions () with - | (id,([concl],strength)) -> id,strength,concl - | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement.") - let solve ?with_end_tac gi info_lvl tac pr = try let tac = match with_end_tac with diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 5699320af5..29ab00876a 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -34,11 +34,6 @@ val get_current_goal_context : unit -> Evd.evar_map * env val get_current_context : ?p:Proof.t -> unit -> Evd.evar_map * env -(** [current_proof_statement] *) - -val current_proof_statement : - unit -> Id.t * goal_kind * EConstr.types - (** {6 ... } *) (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th diff --git a/proofs/proof.ml b/proofs/proof.ml index 4ce932b93d..e40940f652 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -415,8 +415,9 @@ let run_tactic env tac pr = Proofview.Unsafe.tclEVARS sigma >>= fun () -> Proofview.tclUNIT retrieved in + let { name; poly } = pr in let (retrieved,proofview,(status,to_shelve,give_up),info_trace) = - Proofview.apply env tac sp + Proofview.apply ~name ~poly env tac sp in let sigma = Proofview.return proofview in let to_shelve = undef sigma to_shelve in @@ -498,7 +499,8 @@ module V82 = struct let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in Proofview.Unsafe.tclEVARS sigma end in - let ((), proofview, _, _) = Proofview.apply env tac pr.proofview in + let { name; poly } = pr in + let ((), proofview, _, _) = Proofview.apply ~name ~poly env tac pr.proofview in let shelf = List.filter begin fun g -> Evd.is_undefined (Proofview.return proofview) g diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 9ee9e7ae2c..0cfc010c1a 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -66,12 +66,6 @@ let pstates = ref ([] : pstate list) (* combinators for the current_proof lists *) let push a l = l := a::!l -exception NoSuchProof -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 | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") @@ -91,6 +85,7 @@ let cur_pstate () = let give_me_the_proof () = (cur_pstate ()).proof let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None let get_current_proof_name () = (Proof.data (cur_pstate ()).proof).Proof.name +let get_current_persistence () = (cur_pstate ()).strength let with_current_proof f = match !pstates with @@ -386,15 +381,6 @@ let set_terminator hook = | [] -> raise NoCurrentProof | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps -module V82 = struct - let get_current_initial_conclusions () = - let { proof; strength } = cur_pstate () in - let Proof.{ name; entry } = Proof.data proof in - let initial = Proofview.initial_goals entry in - let goals = List.map (fun (o, c) -> c) initial in - name, (goals, strength) -end - let freeze ~marshallable = if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.") else !pstates diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 40920f51a3..38e234eaee 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -17,6 +17,7 @@ val there_are_pending_proofs : unit -> bool val check_no_pending_proof : unit -> unit val get_current_proof_name : unit -> Names.Id.t +val get_current_persistence : unit -> Decl_kinds.goal_kind val get_all_proof_names : unit -> Names.Id.t list val discard : Names.lident -> unit @@ -104,8 +105,6 @@ val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> val get_terminator : unit -> proof_terminator val set_terminator : proof_terminator -> unit -exception NoSuchProof - val get_open_goals : unit -> int (** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is @@ -129,11 +128,6 @@ 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 -module V82 : sig - val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list * - Decl_kinds.goal_kind) -end - val freeze : marshallable:bool -> t val unfreeze : t -> unit val proof_of_state : t -> Proof.t diff --git a/proofs/refine.ml b/proofs/refine.ml index 1d796fece5..06e6b89df1 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -137,26 +137,6 @@ let refine ~typecheck f = in Proofview.Goal.enter (make_refine_enter ~typecheck f) -(** Useful definitions *) - -let with_type env evd c t = - let my_type = Retyping.get_type_of env evd c in - let j = Environ.make_judge c my_type in - let (evd,j') = - Coercion.inh_conv_coerce_to true env evd j t - in - evd , j'.Environ.uj_val - -let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let env = Proofview.Goal.env gl in - let f h = - let (h, c) = f h in - with_type env h c concl - in - refine ~typecheck f -end - (** {7 solve_constraints} Ensure no remaining unification problems are left. Run at every "." by default. *) diff --git a/proofs/refine.mli b/proofs/refine.mli index 1af6463a02..55dafe521f 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -34,17 +34,6 @@ val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic -> Proofview.Goal.t -> 'a tactic (** The general version of refine. *) -(** {7 Helper functions} *) - -val with_type : Environ.env -> Evd.evar_map -> - EConstr.constr -> EConstr.types -> Evd.evar_map * EConstr.constr -(** [with_type env sigma c t] ensures that [c] is of type [t] - inserting a coercion if needed. *) - -val refine_casted : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic -(** Like {!refine} except the refined term is coerced to the conclusion of the - current goal. *) - (** {7 Unification constraint handling} *) val solve_constraints : unit tactic |