diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 24 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 163 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 90 | ||||
| -rw-r--r-- | proofs/refine.ml | 5 | ||||
| -rw-r--r-- | proofs/refine.mli | 3 | ||||
| -rw-r--r-- | proofs/refiner.ml | 55 | ||||
| -rw-r--r-- | proofs/refiner.mli | 29 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 9 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 4 |
10 files changed, 83 insertions, 301 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 66b47a64a7..0662354daf 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -42,11 +42,11 @@ let get_goal_context_gen pf i = (sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) let get_goal_context pf i = - let p = Proof_global.give_me_the_proof pf in + let p = Proof_global.get_proof pf in get_goal_context_gen p i let get_current_goal_context pf = - let p = Proof_global.give_me_the_proof pf in + let p = Proof_global.get_proof pf in try get_goal_context_gen p 1 with | NoSuchGoal -> @@ -57,7 +57,7 @@ let get_current_goal_context pf = Evd.from_env env, env let get_current_context pf = - let p = Proof_global.give_me_the_proof pf in + let p = Proof_global.get_proof pf in try get_goal_context_gen p 1 with | NoSuchGoal -> @@ -108,7 +108,7 @@ let solve ?with_end_tac gi info_lvl tac pr = in (p,status) -let by tac = Proof_global.with_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac) +let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None tac) (**********************************************************************) (* Shortcut to build a term using tactics *) @@ -117,15 +117,14 @@ open Decl_kinds let next = let n = ref 0 in fun () -> incr n; !n -let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac = +let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehavior, false, Proof Theorem) typ tac = let evd = Evd.from_ctx ctx in - let terminator = Proof_global.make_terminator (fun _ -> ()) in let goals = [ (Global.env_of_context sign , typ) ] in - let pf = Proof_global.start_proof evd id goal_kind goals terminator in + let pf = Proof_global.start_proof evd id goal_kind goals in try let pf, status = by tac pf in let open Proof_global in - let { entries; universes } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in + let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in match entries with | [entry] -> let univs = UState.demote_seff_univs entry universes in @@ -139,13 +138,13 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in - let gk = Global, poly, Proof Theorem in + let gk = Global ImportDefaultBehavior, poly, Proof Theorem in let ce, status, univs = build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in - let body = Future.force ce.const_entry_body in + let body, eff = Future.force ce.const_entry_body in let (cb, ctx) = - if side_eff then Safe_typing.inline_private_constants env body - else fst body + if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) + else body in let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in cb, status, univs @@ -196,5 +195,6 @@ let refine_by_tactic ~name ~poly env sigma ty tac = other goals that were already present during its invocation, so that those goals rely on effects that are not present anymore. Hopefully, this hack will work in most cases. *) + let neff = neff.Evd.seff_private in let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in ans, sigma diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 77d701b41f..63d5adfcd2 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -61,7 +61,7 @@ val use_unification_heuristics : unit -> bool val build_constant_by_tactic : Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind -> EConstr.types -> unit Proofview.tactic -> - Safe_typing.private_constants Entries.definition_entry * bool * + Evd.side_effects Entries.definition_entry * bool * UState.t val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic -> diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index b642e8eea7..96d90e9252 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -29,74 +29,31 @@ type lemma_possible_guards = int list list type proof_object = { id : Names.Id.t; - entries : Safe_typing.private_constants Entries.definition_entry list; + entries : Evd.side_effects Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: UState.t; } type opacity_flag = Opaque | Transparent -type proof_ending = - | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of opacity_flag * - lident option * - proof_object - -type proof_terminator = proof_ending -> unit -type closed_proof = proof_object * proof_terminator - -type t = { - terminator : proof_terminator CEphemeron.key; - endline_tactic : Genarg.glob_generic_argument option; - section_vars : Constr.named_context option; - proof : Proof.t; - universe_decl: UState.universe_decl; - strength : Decl_kinds.goal_kind; -} - -(* The head of [t] is the actual current proof, the other ones are - to be resumed when the current proof is closed or aborted. *) -type stack = t * t list - -let pstate_map f (pf, pfl) = (f pf, List.map f pfl) - -let make_terminator f = f -let apply_terminator f = f - -let get_current_pstate (ps,_) = ps - -(* combinators for the current_proof lists *) -let push ~ontop a = - match ontop with - | None -> a , [] - | Some (l,ls) -> a, (l :: ls) - -let maybe_push ~ontop = function - | Some pstate -> Some (push ~ontop pstate) - | None -> ontop +type t = + { endline_tactic : Genarg.glob_generic_argument option + ; section_vars : Constr.named_context option + ; proof : Proof.t + ; universe_decl: UState.universe_decl + ; strength : Decl_kinds.goal_kind + } (*** Proof Global manipulation ***) -let get_all_proof_names (pf : stack) = - let (pn, pns) = pstate_map Proof.(function pf -> (data pf.proof).name) pf in - pn :: pns - -let give_me_the_proof ps = ps.proof -let get_current_proof_name ps = (Proof.data ps.proof).Proof.name -let get_current_persistence ps = ps.strength - -let with_current_pstate f (ps,psl) = - let ps, ret = f ps in - (ps, psl), ret +let get_proof ps = ps.proof +let get_proof_name ps = (Proof.data ps.proof).Proof.name +let get_persistence ps = ps.strength -let modify_current_pstate f (ps,psl) = - f ps, psl +let map_proof f p = { p with proof = f p.proof } +let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res -let modify_proof f ps = - let proof = f ps.proof in - {ps with proof} - -let with_proof f ps = +let map_fold_proof_endline f ps = let et = match ps.endline_tactic with | None -> Proofview.tclUNIT () @@ -111,37 +68,13 @@ let with_proof f ps = let ps = { ps with proof = newpr } in ps, ret -let with_current_proof f (ps,rest) = - let ps, ret = with_proof f ps in - (ps, rest), ret - -let simple_with_current_proof f pf = - let p, () = with_current_proof (fun t p -> f t p , ()) pf in p - -let simple_with_proof f ps = - let ps, () = with_proof (fun t ps -> f t ps, ()) ps in ps - -let compact_the_proof pf = simple_with_proof (fun _ -> Proof.compact) pf +let compact_the_proof pf = map_proof Proof.compact pf (* Sets the tactic to be used when a tactic line is closed with [...] *) let set_endline_tactic tac ps = { ps with endline_tactic = Some tac } -let pf_name_eq id ps = - let Proof.{ name } = Proof.data ps.proof in - Id.equal name id - -let discard {CAst.loc;v=id} (ps, psl) = - match List.filter (fun pf -> not (pf_name_eq id pf)) (ps :: psl) with - | [] -> None - | ps :: psl -> Some (ps, psl) - -let discard_current (_, psl) = - match psl with - | [] -> None - | ps :: psl -> Some (ps, psl) - -(** [start_proof sigma id pl str goals terminator] starts a proof of name +(** [start_proof sigma id pl str goals] 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 @@ -149,21 +82,21 @@ let discard_current (_, psl) = 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. *) -let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator = - { terminator = CEphemeron.create terminator; - proof = Proof.start ~name ~poly:(pi2 kind) sigma goals; - endline_tactic = None; - section_vars = None; - universe_decl = pl; - strength = kind } - -let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator = - { terminator = CEphemeron.create terminator; - proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals; - endline_tactic = None; - section_vars = None; - universe_decl = pl; - strength = kind } +let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals = + { proof = Proof.start ~name ~poly:(pi2 kind) sigma goals + ; endline_tactic = None + ; section_vars = None + ; universe_decl = pl + ; strength = kind + } + +let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals = + { proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals + ; endline_tactic = None + ; section_vars = None + ; universe_decl = pl + ; strength = kind + } let get_used_variables pf = pf.section_vars let get_universe_decl pf = pf.universe_decl @@ -201,7 +134,7 @@ let get_open_goals ps = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + List.length shelf -type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t +type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t let private_poly_univs = let b = ref true in @@ -217,7 +150,7 @@ let private_poly_univs = let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now (fpl : closed_proof_output Future.computation) ps = - let { section_vars; proof; terminator; universe_decl; strength } = ps in + let { section_vars; proof; universe_decl; strength } = ps in let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in let opaque = match opaque with Opaque -> true | Transparent -> false in let constrain_variables ctx = @@ -239,7 +172,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let body = c in let allow_deferred = not poly && (keep_body_ucst_separate || - not (Safe_typing.empty_private_constants = eff)) + not (Safe_typing.empty_private_constants = eff.Evd.seff_private)) in let typ = if allow_deferred then t else nf t in let used_univs_body = Vars.universes_of_constr body in @@ -312,8 +245,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now in let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in { id = name; entries = entries; persistence = strength; - universes }, - fun pr_ending -> CEphemeron.get terminator pr_ending + universes } let return_proof ?(allow_partial=false) ps = let { proof } = ps in @@ -351,22 +283,9 @@ let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps = close_proof ~opaque ~keep_body_ucst_separate ~now:true (Future.from_val ~fix_exn (return_proof ps)) ps -(** Gets the current terminator without checking that the proof has - been completed. Useful for the likes of [Admitted]. *) -let get_terminator ps = CEphemeron.get ps.terminator -let set_terminator hook ps = - { ps with terminator = CEphemeron.create hook } - -let copy_terminators ~src ~tgt = - let (ps, psl), (ts,tsl) = src, tgt in - assert(List.length psl = List.length tsl); - {ts with terminator = ps.terminator}, List.map2 (fun op p -> { p with terminator = op.terminator }) psl tsl - -let update_global_env pf = - let res, () = - with_proof (fun _ p -> - Proof.in_proof p (fun sigma -> - let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in - let (p,(status,info),()) = Proof.run_tactic (Global.env ()) tac p in - (p, ()))) pf - in res +let update_global_env = + map_proof (fun p -> + Proof.in_proof p (fun sigma -> + let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in + let p,(status,info),_ = Proof.run_tactic (Global.env ()) tac p in + p)) diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index aff48b9636..f84ec27df7 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -13,18 +13,16 @@ environment. *) type t -type stack -val get_current_pstate : stack -> t - -val get_current_proof_name : t -> Names.Id.t -val get_current_persistence : t -> Decl_kinds.goal_kind -val get_all_proof_names : stack -> Names.Id.t list +(* Should be moved into a proper view *) +val get_proof : t -> Proof.t +val get_proof_name : t -> Names.Id.t +val get_persistence : t -> Decl_kinds.goal_kind +val get_used_variables : t -> Constr.named_context option -val discard : Names.lident -> stack -> stack option -val discard_current : stack -> stack option +(** Get the universe declaration associated to the current proof. *) +val get_universe_decl : t -> UState.universe_decl -val give_me_the_proof : t -> Proof.t val compact_the_proof : t -> t (** When a proof is closed, it is reified into a [proof_object], where @@ -37,30 +35,14 @@ type lemma_possible_guards = int list list type proof_object = { id : Names.Id.t; - entries : Safe_typing.private_constants Entries.definition_entry list; + entries : Evd.side_effects Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: UState.t; } type opacity_flag = Opaque | Transparent -type proof_ending = - | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * - UState.t - | Proved of opacity_flag * - Names.lident option * - proof_object -type proof_terminator -type closed_proof = proof_object * proof_terminator - -val make_terminator : (proof_ending -> unit) -> proof_terminator -val apply_terminator : proof_terminator -> proof_ending -> unit - -val push : ontop:stack option -> t -> stack - -val maybe_push : ontop:stack option -> t option -> stack option - -(** [start_proof ~ontop id str pl goals terminator] starts a proof of name +(** [start_proof id str pl goals] 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; [terminator] is used at the end of the proof to close the proof @@ -68,16 +50,22 @@ val maybe_push : ontop:stack option -> t option -> stack option morphism). 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:UState.universe_decl -> - Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list -> - proof_terminator -> t +val start_proof + : Evd.evar_map + -> Names.Id.t + -> ?pl:UState.universe_decl + -> Decl_kinds.goal_kind + -> (Environ.env * EConstr.types) list + -> t (** Like [start_proof] except that there may be dependencies between initial goals. *) -val start_dependent_proof : - Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> - Proofview.telescope -> proof_terminator -> t +val start_dependent_proof + : Names.Id.t + -> ?pl:UState.universe_decl + -> Decl_kinds.goal_kind + -> Proofview.telescope + -> t (** Update the proofs global environment after a side-effecting command (e.g. a sublemma definition) has been run inside it. Assumes @@ -86,40 +74,25 @@ val update_global_env : t -> t (* Takes a function to add to the exceptions data relative to the state in which the proof was built *) -val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> - t -> closed_proof +val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> proof_object (* Intermediate step necessary to delegate the future. * Both access the current proof state. The former is supposed to be * chained with a computation that completed the proof *) -type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t +type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t (* 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 -> t -> closed_proof_output val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t -> - closed_proof_output Future.computation -> closed_proof + closed_proof_output Future.computation -> proof_object -(** Gets the current terminator without checking that the proof has - been completed. Useful for the likes of [Admitted]. *) -val get_terminator : t -> proof_terminator -val set_terminator : proof_terminator -> t -> t val get_open_goals : t -> int -(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is - no current proof. - The return boolean is set to [false] if an unsafe tactic has been used. *) -val with_current_proof : - (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> stack -> stack * 'a -val simple_with_current_proof : - (unit Proofview.tactic -> Proof.t -> Proof.t) -> stack -> stack - -val with_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a -val modify_proof : (Proof.t -> Proof.t) -> t -> t - -val with_current_pstate : (t -> t * 'a) -> stack -> stack * 'a -val modify_current_pstate : (t -> t) -> stack -> stack +val map_proof : (Proof.t -> Proof.t) -> t -> t +val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a +val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a (** Sets the tactic to be used when a tactic line is closed with [...] *) val set_endline_tactic : Genarg.glob_generic_argument -> t -> t @@ -129,10 +102,3 @@ val set_endline_tactic : Genarg.glob_generic_argument -> t -> t * ids to be cleared *) val set_used_variables : t -> Names.Id.t list -> (Constr.named_context * Names.lident list) * t - -val get_used_variables : t -> Constr.named_context option - -(** Get the universe declaration associated to the current proof. *) -val get_universe_decl : t -> UState.universe_decl - -val copy_terminators : src:stack -> tgt:stack -> stack diff --git a/proofs/refine.ml b/proofs/refine.ml index 4a9404aa96..d0e89183a8 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -60,7 +60,7 @@ let generic_refine ~typecheck f gl = let evs = Evd.save_future_goals sigma in (* Redo the effects in sigma in the monad's env *) let privates_csts = Evd.eval_side_effects sigma in - let env = Safe_typing.push_private_constants env privates_csts in + let env = Safe_typing.push_private_constants env privates_csts.Evd.seff_private in (* Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in @@ -116,9 +116,6 @@ let lift c = let make_refine_enter ~typecheck f gl = generic_refine ~typecheck (lift f) gl -let refine_one ~typecheck f = - Proofview.Goal.enter_one (make_refine_enter ~typecheck f) - let refine ~typecheck f = let f evd = let (evd,c) = f evd in (evd,((), c)) diff --git a/proofs/refine.mli b/proofs/refine.mli index b8948a92f3..93fd9d7a64 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -27,9 +27,6 @@ val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> uni raised during the interpretation of [t] are caught and result in tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) -val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic -(** A variant of [refine] which assumes exactly one goal under focus *) - val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic -> Proofview.Goal.t -> 'a tactic (** The general version of refine. *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 799f4a380b..557f428be9 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -129,9 +129,6 @@ let tclTHENSLASTn tac1 tac taci = tclTHENS3PARTS tac1 [||] tac taci let tclTHEN_i tac taci gls = finish_tac (thensi_tac taci (then_tac tac (start_tac gls))) -let tclTHENLASTn tac1 taci = tclTHENSLASTn tac1 tclIDTAC taci -let tclTHENFIRSTn tac1 taci = tclTHENSFIRSTn tac1 taci tclIDTAC - (* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) let tclTHEN tac1 tac2 = tclTHENS3PARTS tac1 [||] tac2 [||] @@ -253,46 +250,9 @@ let rec tclFIRST = function | [] -> tclFAIL_s "No applicable tactic." | t::rest -> tclORELSE0 t (tclFIRST rest) -let ite_gen tcal tac_if continue tac_else gl= - let success=ref false in - let tac_if0 gl= - let result=tac_if gl in - success:=true;result in - let tac_else0 e gl= - if !success then - iraise e - else - try - tac_else gl - with - e' when CErrors.noncritical e' -> iraise e in - try - tcal tac_if0 continue gl - with (* Breakpoint *) - | e when CErrors.noncritical e -> - let e = CErrors.push e in catch_failerror e; tac_else0 e gl - -(* Try the first tactic and, if it succeeds, continue with - the second one, and if it fails, use the third one *) - -let tclIFTHENELSE=ite_gen tclTHEN - -(* Idem with tclTHENS and tclTHENSV *) - -let tclIFTHENSELSE=ite_gen tclTHENS - -let tclIFTHENSVELSE=ite_gen tclTHENSV - -let tclIFTHENTRYELSEMUST tac1 tac2 gl = - tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl - (* Fails if a tactic did not solve the goal *) let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") -(* Try the first that solves the current goal *) -let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) - - (* Iteration tacticals *) let tclDO n t = @@ -311,22 +271,7 @@ let rec tclREPEAT t g = let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) -(* Repeat on the first subgoal (no failure if no more subgoal) *) -let rec tclREPEAT_MAIN t g = - (tclORELSE (tclTHEN_i t (fun i -> if Int.equal i 1 then (tclREPEAT_MAIN t) else - tclIDTAC)) tclIDTAC) g - (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} - -let tclEVARUNIVCONTEXT ctx gls = tclIDTAC {gls with sigma= Evd.set_universe_context gls.sigma ctx} - -(* Push universe context *) -let tclPUSHCONTEXT rigid ctx tac gl = - tclTHEN (tclEVARS (Evd.merge_context_set rigid (project gl) ctx)) tac gl - let tclPUSHEVARUNIVCONTEXT ctx gl = tclEVARS (Evd.merge_universe_context (project gl) ctx) gl - -let tclPUSHCONSTRAINTS cst gl = - tclEVARS (Evd.add_constraints (project gl) cst) gl diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 52cbf7658b..0f34a79c49 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -32,12 +32,8 @@ val tclIDTAC_MESSAGE : Pp.t -> tactic (** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic -val tclEVARUNIVCONTEXT : UState.t -> tactic - -val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic -val tclPUSHCONSTRAINTS : Univ.Constraint.t -> tactic (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) @@ -86,16 +82,6 @@ val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic [tac2] for the remaining last subgoals (previously called tclTHENST) *) val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic -(** [tclTHENLASTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, - applies [t1],...,[tn] on the last [n] resulting subgoals and leaves - unchanged the other subgoals *) -val tclTHENLASTn : tactic -> tactic array -> tactic - -(** [tclTHENFIRSTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, - applies [t1],...,[tn] on the first [n] resulting subgoals and leaves - unchanged the other subgoals (previously called [tclTHENSI]) *) -val tclTHENFIRSTn : tactic -> tactic array -> tactic - (** A special exception for levels for the Fail tactic *) exception FailError of int * Pp.t Lazy.t @@ -106,9 +92,7 @@ val catch_failerror : Exninfo.iexn -> unit val tclORELSE0 : tactic -> tactic -> tactic val tclORELSE : tactic -> tactic -> tactic val tclREPEAT : tactic -> tactic -val tclREPEAT_MAIN : tactic -> tactic val tclFIRST : tactic list -> tactic -val tclSOLVE : tactic list -> tactic val tclTRY : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclCOMPLETE : tactic -> tactic @@ -118,16 +102,3 @@ val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic val tclDO : int -> tactic -> tactic val tclPROGRESS : tactic -> tactic val tclSHOWHYPS : tactic -> tactic - -(** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then, - if it succeeds, applies [tac2] to the resulting subgoals, - and if not applies [tac3] to the initial goal [gls] *) -val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic -val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic -val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic - -(** [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1] - has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed. - Equivalent to [(tac1;try tac2)||tac2] *) - -val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 93031c2202..d7b4f729cb 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -81,12 +81,10 @@ let pf_type_of = pf_reduce type_of let pf_get_type_of = pf_reduce Retyping.get_type_of let pf_conv_x gl = pf_reduce test_conversion gl Reduction.CONV -let pf_conv_x_leq gl = pf_reduce test_conversion gl Reduction.CUMUL let pf_const_value = pf_reduce (fun env _ c -> EConstr.of_constr (constant_value_in env c)) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind - let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls (* Pretty-printers *) @@ -181,14 +179,7 @@ module New = struct let pf_hnf_type_of gl t = pf_whd_all gl (pf_get_type_of gl t) - let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t let pf_nf_evar gl t = nf_evar (project gl) t - - let pf_undefined_evars gl = - let sigma = Proofview.Goal.sigma gl in - let ev = Proofview.Goal.goal gl in - let evi = Evd.find sigma ev in - Evarutil.filtered_undefined_evars_of_evar_info sigma evi end diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 23e1e6f566..195be04986 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -64,7 +64,6 @@ val pf_unfoldn : (occurrences * evaluable_global_reference) list val pf_const_value : Goal.goal sigma -> pconstant -> constr val pf_conv_x : Goal.goal sigma -> constr -> constr -> bool -val pf_conv_x_leq : Goal.goal sigma -> constr -> constr -> bool (** {6 Pretty-printing functions (debug only). } *) val pr_gls : Goal.goal sigma -> Pp.t @@ -109,11 +108,8 @@ module New : sig val pf_hnf_constr : Proofview.Goal.t -> constr -> types val pf_hnf_type_of : Proofview.Goal.t -> constr -> types - val pf_whd_all : Proofview.Goal.t -> constr -> constr val pf_compute : Proofview.Goal.t -> constr -> constr val pf_nf_evar : Proofview.Goal.t -> constr -> constr - (** Gathers the undefined evars of the given goal. *) - val pf_undefined_evars : Proofview.Goal.t -> Evar.Set.t end |