diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.mli | 2 | ||||
| -rw-r--r-- | proofs/goal.ml | 2 | ||||
| -rw-r--r-- | proofs/goal.mli | 2 | ||||
| -rw-r--r-- | proofs/logic.ml | 1 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 8 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 6 | ||||
| -rw-r--r-- | proofs/proof.ml | 11 | ||||
| -rw-r--r-- | proofs/proof.mli | 62 | ||||
| -rw-r--r-- | proofs/proof_bullet.ml | 8 | ||||
| -rw-r--r-- | proofs/proof_bullet.mli | 10 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 54 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 24 | ||||
| -rw-r--r-- | proofs/refiner.mli | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 5 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 8 |
15 files changed, 97 insertions, 108 deletions
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index a0e3b718a2..d90cff5722 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -14,5 +14,5 @@ open Ltac_pretype type glob_constr_ltac_closure = ltac_var_map * glob_constr -val w_refine : evar * evar_info -> +val w_refine : Evar.t * evar_info -> glob_constr_ltac_closure -> evar_map -> evar_map diff --git a/proofs/goal.ml b/proofs/goal.ml index 19f816a019..d5bc7e0ce2 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -16,7 +16,7 @@ module NamedDecl = Context.Named.Declaration evar is defined in the current evar_map, should not be accessed. *) (* type of the goals *) -type goal = Evd.evar +type goal = Evar.t let pr_goal e = str "GOAL:" ++ Pp.int (Evar.repr e) diff --git a/proofs/goal.mli b/proofs/goal.mli index ad968cdfb3..37dd9d3c0c 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -58,7 +58,7 @@ module V82 : sig (* Principal part of the progress tactical *) val progress : goal list Evd.sigma -> goal Evd.sigma -> bool - + (* Principal part of tclNOTSAMEGOAL *) val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool diff --git a/proofs/logic.ml b/proofs/logic.ml index 13a4e4ce31..a9ad606a03 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -11,7 +11,6 @@ open CErrors open Util open Names open Nameops -open Term open Constr open Vars open Termops diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 2d4aba17cb..6b503a0112 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -51,9 +51,8 @@ end let get_nth_V82_goal i = let p = Proof_global.give_me_the_proof () in - let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in - try - { it=(List.nth goals (i-1)) ; sigma=sigma; } + let goals,_,_,_,sigma = Proof.proof p in + try { it = List.nth goals (i-1) ; sigma } with Failure _ -> raise NoSuchGoal let get_goal_context_gen i = @@ -141,7 +140,8 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo let status = by tac in let _,(const,univs,_) = cook_proof () in Proof_global.discard_current (); - const, status, fst univs + let univs = UState.demote_seff_univs const univs in + const, status, univs with reraise -> let reraise = CErrors.push reraise in Proof_global.discard_current (); diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index d676a0874b..5a317a956d 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -35,11 +35,11 @@ val start_proof : val cook_this_proof : Proof_global.proof_object -> (Id.t * - (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind)) val cook_proof : unit -> (Id.t * - (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind)) (** {6 ... } *) (** [get_goal_context n] returns the context of the [n]th subgoal of @@ -74,7 +74,7 @@ val current_proof_statement : val solve : ?with_end_tac:unit Proofview.tactic -> Vernacexpr.goal_selector -> int option -> unit Proofview.tactic -> - Proof.proof -> Proof.proof*bool + Proof.t -> Proof.t * bool (** [by tac] applies tactic [tac] to the 1st subgoal of the current focused proof or raises a UserError if there is no focused proof or diff --git a/proofs/proof.ml b/proofs/proof.ml index e24d57f088..04e707cd66 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -98,7 +98,7 @@ let done_cond ?(loose_end=false) k = CondDone (loose_end,k) (* Subpart of the type of proofs. It contains the parts of the proof which are under control of the undo mechanism *) -type proof = { +type t = { (* Current focused proofview *) proofview: Proofview.proofview; (* Entry for the proofview *) @@ -115,6 +115,8 @@ type proof = { initial_euctx : UState.t } +type proof = t + (*** General proof functions ***) let proof p = @@ -163,6 +165,7 @@ let map_structured_proof pfts process_goal: 'a pre_goals = let rec unroll_focus pv = function | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk | [] -> pv + (* spiwack: a proof is considered completed even if its still focused, if the focus doesn't hide any goal. Unfocusing is handled in {!return}. *) @@ -391,10 +394,12 @@ let pr_proof p = (*** Compatibility layer with <=v8.2 ***) module V82 = struct let subgoals p = - Proofview.V82.goals p.proofview + let it, sigma = Proofview.proofview p.proofview in + Evd.{ it; sigma } let background_subgoals p = - Proofview.V82.goals (unroll_focus p.proofview p.focus_stack) + let it, sigma = Proofview.proofview (unroll_focus p.proofview p.focus_stack) in + Evd.{ it; sigma } let top_goal p = let { Evd.it=gls ; sigma=sigma; } = diff --git a/proofs/proof.mli b/proofs/proof.mli index 48aed8225e..0b5e771ef3 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -30,7 +30,9 @@ *) (* Type of a proof. *) -type proof +type t +type proof = t +[@@ocaml.deprecated "please use [Proof.t]"] (* Returns a stylised view of a proof for use by, for instance, ide-s. *) @@ -42,7 +44,7 @@ type proof shelf (the list of goals on the shelf), a representation of the given up goals (the list of the given up goals) and the underlying evar_map *) -val proof : proof -> +val proof : t -> Goal.goal list * (Goal.goal list * Goal.goal list) list * Goal.goal list @@ -61,27 +63,26 @@ type 'a pre_goals = { (** List of the goals that have been given up *) } -val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) +val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) (*** General proof functions ***) - -val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof -val dependent_start : Proofview.telescope -> proof -val initial_goals : proof -> (EConstr.constr * EConstr.types) list -val initial_euctx : proof -> UState.t +val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> t +val dependent_start : Proofview.telescope -> t +val initial_goals : t -> (EConstr.constr * EConstr.types) list +val initial_euctx : t -> UState.t (* Returns [true] if the considered proof is completed, that is if no goal remain to be considered (this does not require that all evars have been solved). *) -val is_done : proof -> bool +val is_done : t -> bool (* Like is_done, but this time it really means done (i.e. nothing left to do) *) -val is_complete : proof -> bool +val is_complete : t -> bool (* Returns the list of partial proofs to initial goals. *) -val partial_proof : proof -> EConstr.constr list +val partial_proof : t -> EConstr.constr list -val compact : proof -> proof +val compact : t -> t (* Returns the proofs (with their type) of the initial goals. Raises [UnfinishedProof] is some goals remain to be considered. @@ -92,7 +93,7 @@ exception UnfinishedProof exception HasShelvedGoals exception HasGivenUpGoals exception HasUnresolvedEvar -val return : proof -> Evd.evar_map +val return : t -> Evd.evar_map (*** Focusing actions ***) @@ -132,7 +133,7 @@ val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition (* focus command (focuses on the [i]th subgoal) *) (* spiwack: there could also, easily be a focus-on-a-range tactic, is there a need for it? *) -val focus : 'a focus_condition -> 'a -> int -> proof -> proof +val focus : 'a focus_condition -> 'a -> int -> t -> t exception FullyUnfocused exception CannotUnfocusThisWay @@ -148,58 +149,59 @@ exception NoSuchGoals of int * int Raises [FullyUnfocused] if the proof is not focused. Raises [CannotUnfocusThisWay] if the proof the unfocusing condition is not met. *) -val unfocus : 'a focus_kind -> proof -> unit -> proof +val unfocus : 'a focus_kind -> t -> unit -> t (* [unfocused p] returns [true] when [p] is fully unfocused. *) -val unfocused : proof -> bool +val unfocused : t -> bool (* [get_at_focus k] gets the information stored at the closest focus point of kind [k]. Raises [NoSuchFocus] if there is no focus point of kind [k]. *) exception NoSuchFocus -val get_at_focus : 'a focus_kind -> proof -> 'a +val get_at_focus : 'a focus_kind -> t -> 'a (* [is_last_focus k] check if the most recent focus is of kind [k] *) -val is_last_focus : 'a focus_kind -> proof -> bool +val is_last_focus : 'a focus_kind -> t -> bool (* returns [true] if there is no goal under focus. *) -val no_focused_goal : proof -> bool +val no_focused_goal : t -> bool (*** Tactics ***) (* the returned boolean signal whether an unsafe tactic has been used. In which case it is [false]. *) val run_tactic : Environ.env -> - unit Proofview.tactic -> proof -> proof*(bool*Proofview_monad.Info.tree) + unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) -val maximal_unfocus : 'a focus_kind -> proof -> proof +val maximal_unfocus : 'a focus_kind -> t -> t (*** Commands ***) -val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a +val in_proof : t -> (Evd.evar_map -> 'a) -> 'a (* Remove all the goals from the shelf and adds them at the end of the focused goals. *) -val unshelve : proof -> proof +val unshelve : t -> t -val pr_proof : proof -> Pp.t +val pr_proof : t -> Pp.t (*** Compatibility layer with <=v8.2 ***) module V82 : sig - val subgoals : proof -> Goal.goal list Evd.sigma + val subgoals : t -> Goal.goal list Evd.sigma + [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"] (* All the subgoals of the proof, including those which are not focused. *) - val background_subgoals : proof -> Goal.goal list Evd.sigma + val background_subgoals : t -> Goal.goal list Evd.sigma - val top_goal : proof -> Goal.goal Evd.sigma + val top_goal : t -> Goal.goal Evd.sigma (* returns the existential variable used to start the proof *) - val top_evars : proof -> Evd.evar list + val top_evars : t -> Evar.t list (* Turns the unresolved evars into goals. Raises [UnfinishedProof] if there are still unsolved goals. *) - val grab_evars : proof -> proof + val grab_evars : t -> t (* Implements the Existential command *) - val instantiate_evar : int -> Constrexpr.constr_expr -> proof -> proof + val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t end diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 4f575ab4be..2149163314 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -25,8 +25,8 @@ let pr_bullet b = type behavior = { name : string; - put : proof -> t -> proof; - suggest: proof -> Pp.t + put : Proof.t -> t -> Proof.t; + suggest: Proof.t -> Pp.t } let behaviors = Hashtbl.create 4 @@ -110,7 +110,7 @@ module Strict = struct let push (b:t) pr = focus bullet_cond (b::get_bullets pr) 1 pr - let suggest_bullet (prf : proof): suggestion = + let suggest_bullet (prf : Proof.t): suggestion = if is_done prf then ProofFinished else if not (no_focused_goal prf) then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *) @@ -137,7 +137,7 @@ module Strict = struct in loop prf - let rec pop_until (prf : proof) bul : proof = + let rec pop_until (prf : Proof.t) bul : Proof.t = let prf', b = pop prf in if bullet_eq bul b then prf' else pop_until prf' bul diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli index 9e924fec97..09fcabf50a 100644 --- a/proofs/proof_bullet.mli +++ b/proofs/proof_bullet.mli @@ -12,8 +12,6 @@ (* *) (**********************************************************) -open Proof - type t = Vernacexpr.bullet (** A [behavior] is the data of a put function which @@ -22,8 +20,8 @@ type t = Vernacexpr.bullet with a name to identify the behavior. *) type behavior = { name : string; - put : proof -> t -> proof; - suggest: proof -> Pp.t + put : Proof.t -> t -> Proof.t; + suggest: Proof.t -> Pp.t } (** A registered behavior can then be accessed in Coq @@ -39,8 +37,8 @@ val register_behavior : behavior -> unit (** Handles focusing/defocusing with bullets: *) -val put : proof -> t -> proof -val suggest : proof -> Pp.t +val put : Proof.t -> t -> Proof.t +val suggest : Proof.t -> Pp.t (**********************************************************) (* *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index fdc9a236bf..167d6bda0d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -68,17 +68,16 @@ let _ = (* Extra info on proofs. *) type lemma_possible_guards = int list list -type proof_universes = UState.t * Universes.universe_binders option type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - universes: proof_universes; + universes: UState.t; } type proof_ending = - | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes + | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t | Proved of Vernacexpr.opacity_flag * Vernacexpr.lident option * proof_object @@ -90,12 +89,15 @@ type pstate = { terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; section_vars : Context.Named.t option; - proof : Proof.proof; + proof : Proof.t; strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; universe_decl: Univdecls.universe_decl; } +type t = pstate list +type state = t + let make_terminator f = f let apply_terminator f = f @@ -316,10 +318,6 @@ let get_open_goals () = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + List.length shelf -let constrain_variables init uctx = - let levels = Univ.Instance.levels (Univ.UContext.instance init) in - UState.constrain_variables levels uctx - type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t let close_proof ~keep_body_ucst_separate ?feedback_id ~now @@ -329,10 +327,11 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in let initial_euctx = Proof.initial_euctx proof in + let constrain_variables ctx = + UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx + in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in - let binders, univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in - let binders = if poly then Some binders else None in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) @@ -348,20 +347,21 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then nf t else t - in - let used_univs_body = Univops.universes_of_constr body in - let used_univs_typ = Univops.universes_of_constr typ in + 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 if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then - let initunivs = Evd.evar_context_universe_context initial_euctx in - let ctx = constrain_variables initunivs universes in + let initunivs = UState.const_univ_entry ~poly initial_euctx in + let ctx = constrain_variables universes in (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of the body. So we keep the two sets distinct. *) - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx_body = UState.restrict ctx used_univs in - let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in - (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff) + let univs = UState.check_mono_univ_decl ctx_body universe_decl in + (initunivs, typ), ((body, univs), 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 @@ -370,30 +370,28 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now TODO: check if restrict is really necessary now. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx = UState.restrict universes used_univs in - let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in + let univs = UState.check_univ_decl ~poly ctx universe_decl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in fun t p -> Future.split2 (Future.chain p (make_body t)) else fun t p -> + (* Already checked the univ_decl for the type universes when starting the proof. *) + let univctx = Entries.Monomorphic_const_entry (UState.context_set universes) in Future.from_val (univctx, nf t), Future.chain p (fun (pt,eff) -> (* Deferred proof, we already checked the universe declaration with the initial universes, ensure that the final universes respect the declaration as well. If the declaration is non-extensible, this will prevent the body from adding universes and constraints. *) - let bodyunivs = constrain_variables univctx (Future.force univs) in - let _, univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in - (pt,Univ.ContextSet.of_context univs),eff) + let bodyunivs = constrain_variables (Future.force univs) in + let univs = UState.check_mono_univ_decl bodyunivs universe_decl in + (pt,univs),eff) in let entry_fn p (_, t) = let t = EConstr.Unsafe.to_constr t in let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in - let univs = - if poly then Entries.Polymorphic_const_entry univs - else Entries.Monomorphic_const_entry univs - in {Entries. const_entry_body = body; const_entry_secctx = section_vars; @@ -405,7 +403,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now in let entries = Future.map2 entry_fn fpl initial_goals in { id = pid; entries = entries; persistence = strength; - universes = (universes, binders) }, + universes }, fun pr_ending -> CEphemeron.get terminator pr_ending let return_proof ?(allow_partial=false) () = @@ -466,8 +464,6 @@ module V82 = struct pid, (goals, strength) end -type state = pstate list - let freeze ~marshallable = match marshallable with | `Yes -> diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index eed62f912e..27e99f218b 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -10,6 +10,10 @@ toplevel. In particular it defines the global proof environment. *) +type t +type state = t +[@@ocaml.deprecated "please use [Proof_global.t]"] + val there_are_pending_proofs : unit -> bool val check_no_pending_proof : unit -> unit @@ -21,7 +25,7 @@ val discard_current : unit -> unit val discard_all : unit -> unit exception NoCurrentProof -val give_me_the_proof : unit -> Proof.proof +val give_me_the_proof : unit -> Proof.t (** @raise NoCurrentProof when outside proof mode. *) val compact_the_proof : unit -> unit @@ -33,18 +37,17 @@ val compact_the_proof : unit -> unit (i.e. an proof ending command) and registers the appropriate values. *) type lemma_possible_guards = int list list -type proof_universes = UState.t * Universes.universe_binders option type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - universes: proof_universes; + universes: UState.t; } type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * - proof_universes + UState.t | Proved of Vernacexpr.opacity_flag * Vernacexpr.lident option * proof_object @@ -107,9 +110,9 @@ val get_open_goals : unit -> int 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.proof -> Proof.proof*'a) -> 'a + (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a val simple_with_current_proof : - (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit + (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit (** Sets the tactic to be used when a tactic line is closed with [...] *) val set_endline_tactic : Genarg.glob_generic_argument -> unit @@ -129,11 +132,10 @@ module V82 : sig Decl_kinds.goal_kind) end -type state -val freeze : marshallable:[`Yes | `No | `Shallow] -> state -val unfreeze : state -> unit -val proof_of_state : state -> Proof.proof -val copy_terminators : src:state -> tgt:state -> state +val freeze : marshallable:[`Yes | `No | `Shallow] -> t +val unfreeze : t -> unit +val proof_of_state : t -> Proof.t +val copy_terminators : src:t -> tgt:t -> t (**********************************************************) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 34e517aedc..52dc8bfd8c 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -40,7 +40,7 @@ val tclEVARUNIVCONTEXT : UState.t -> tactic val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic -val tclPUSHCONSTRAINTS : Univ.constraints -> tactic +val tclPUSHCONSTRAINTS : Univ.Constraint.t -> tactic (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a8ec4d8ca3..cab8d7b52a 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -102,9 +102,6 @@ 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 -let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p c -let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c - (********************************************) (* Definition of the most primitive tactics *) (********************************************) @@ -223,8 +220,6 @@ module New = struct let pf_hnf_type_of gl t = pf_whd_all gl (pf_get_type_of gl t) - let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t - let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index d9496d2b4f..e0fb8fbc5d 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -12,9 +12,7 @@ open Environ open EConstr open Proof_type open Redexpr -open Pattern open Locus -open Ltac_pretype (** Operations for handling terms under a local typing context. *) @@ -79,10 +77,6 @@ val pf_const_value : goal sigma -> pconstant -> constr val pf_conv_x : goal sigma -> constr -> constr -> bool val pf_conv_x_leq : goal sigma -> constr -> constr -> bool -val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map -val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool - - (** {6 The most primitive tactics. } *) val refiner : rule -> tactic @@ -138,8 +132,6 @@ module New : sig val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr val pf_compute : 'a Proofview.Goal.t -> constr -> constr - val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr end |