diff options
| -rw-r--r-- | plugins/cc/cctac.ml | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 4 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 2 | ||||
| -rw-r--r-- | proofs/proofview.ml | 225 | ||||
| -rw-r--r-- | proofs/proofview.mli | 115 | ||||
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/autorewrite.ml | 2 | ||||
| -rw-r--r-- | tactics/contradiction.ml | 2 | ||||
| -rw-r--r-- | tactics/coretactics.ml4 | 10 | ||||
| -rw-r--r-- | tactics/equality.ml | 14 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 8 | ||||
| -rw-r--r-- | tactics/inv.ml | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 8 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 36 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 46 |
16 files changed, 249 insertions, 233 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 364a71d28..858c80f29 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -390,7 +390,7 @@ let discriminate_tac (cstr,u as cstru) p = app_global _eq_rect [|outtype;trivial;pred;identity;concl;injt|] k) in let neweq=new_app_global _eq [|intype;t1;t2|] in - Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evm) + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) (Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]) end diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index b28f0652d..2006a2a61 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -834,7 +834,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t = let rl = carg (make_term_list env evdref e.ring_carrier rl) in let lH = carg (make_hyp_list env evdref lH) in let ring = ltac_ring_structure e in - Proofview.tclTHEN (Proofview.V82.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl])) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl])) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end @@ -1150,7 +1150,7 @@ let field_lookup (f:glob_tactic_expr) lH rl t = let rl = carg (make_term_list env evdref e.field_carrier rl) in let lH = carg (make_hyp_list env evdref lH) in let field = ltac_field_structure e in - Proofview.tclTHEN (Proofview.V82.tclEVARS !evdref) (ltac_apply f (field@[lH;rl])) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl])) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 76fc37d37..7d25bb665 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -123,7 +123,7 @@ let unify ?(flags=fail_quick_unif_flags) m = let evd = create_goal_evar_defs (Proofview.Goal.sigma gl) in try let evd' = w_unify env evd CONV ~flags m n in - Proofview.V82.tclEVARSADVANCE evd' + Proofview.Unsafe.tclEVARSADVANCE evd' with e when Errors.noncritical e -> (** This is Tacticals.tclFAIL *) Proofview.tclZERO (FailError (0, lazy (Errors.print e))) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index a3f58396f..4a83ed6d2 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -864,57 +864,7 @@ let in_proofview p k = let reset_future_goals p = { p with solution = Evd.reset_future_goals p.solution } - -module Notations = struct - let (>>=) = tclBIND - let (<*>) = tclTHEN - let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) -end - -open Notations - -module Monad = - Monad.Make(struct type +'a t = 'a tactic let return=tclUNIT let (>>=)=(>>=) end) - - -(*** Compatibility layer with <= 8.2 tactics ***) -module V82 = struct - type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma - - let tactic tac = - (* spiwack: we ignore the dependencies between goals here, - expectingly preserving the semantics of <= 8.2 tactics *) - (* spiwack: convenience notations, waiting for ocaml 3.12 *) - let (>>=) = Proof.bind in - Pv.get >>= fun ps -> - try - let tac gl evd = - let glsigma = - tac { Evd.it = gl ; sigma = evd; } in - let sigma = glsigma.Evd.sigma in - let g = glsigma.Evd.it in - ( g, sigma ) - in - (* Old style tactics expect the goals normalized with respect to evars. *) - let (initgoals,initevd) = - Evd.Monad.List.map (fun g s -> Goal.V82.nf_evar s g) ps.comb ps.solution - in - let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in - let sgs = List.flatten goalss in - Pv.set { solution = evd; comb = sgs; } - with e when catchable_exception e -> - let e = Errors.push e in - tclZERO e - - - (* normalises the evars in the goals, and stores the result in - solution. *) - let nf_evar_goals = - Pv.modify begin fun ps -> - let map g s = Goal.V82.nf_evar s g in - let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in - { solution = evd; comb = goals; } - end +module Unsafe = struct (* A [Proofview.tactic] version of [Refiner.tclEVARS] *) let tclEVARS evd = @@ -925,66 +875,22 @@ module V82 = struct let tclEVARUNIVCONTEXT ctx = Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx }) - - let has_unresolved_evar pv = - Evd.has_undefined pv.solution - - (* Main function in the implementation of Grab Existential Variables.*) - let grab pv = - let undef = Evd.undefined_map pv.solution in - let goals = List.rev_map fst (Evar.Map.bindings undef) in - { pv with comb = goals } - - - (* Returns the open goals of the proofview together with the evar_map to - interprete them. *) - let goals { comb = comb ; solution = solution; } = - { Evd.it = comb ; sigma = solution } - - let top_goals initial { solution=solution; } = - let goals = List.map (fun (t,_) -> fst (Term.destEvar t)) initial in - { Evd.it = goals ; sigma=solution; } - - let top_evars initial = - let evars_of_initial (c,_) = - Evar.Set.elements (Evd.evars_of_term c) - in - List.flatten (List.map evars_of_initial initial) - - let instantiate_evar n com pv = - let (evk,_) = - let evl = Evarutil.non_instantiated pv.solution in - let evl = Evar.Map.bindings evl in - if (n <= 0) then - Errors.error "incorrect existential variable index" - else if List.length evl < n then - Errors.error "not so many uninstantiated existential variables" - else - List.nth evl (n-1) - in - { pv with - solution = Evar_refiner.instantiate_pf_com evk com pv.solution } - - let of_tactic t gls = - try - let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in - let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in - { Evd.sigma = final.solution ; it = final.comb } - with Proofview_monad.TacticFailure e as src -> - let src = Errors.push src in - let e = Backtrace.app_backtrace ~src ~dst:e in - raise e +end - let put_status = Status.put +module Notations = struct + let (>>=) = tclBIND + let (<*>) = tclTHEN + let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) +end - let catchable_exception = catchable_exception +open Notations - let wrap_exceptions f = - try f () - with e when catchable_exception e -> let e = Errors.push e in tclZERO e +module Monad = + Monad.Make(struct type +'a t = 'a tactic let return=tclUNIT let (>>=)=(>>=) end) -end +(* To avoid shadowing by the local [Goal] module *) +module GoalV82 = Goal.V82 module Goal = struct @@ -1022,7 +928,7 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try let (gl, sigma) = nf_gmake env sigma goal in - tclTHEN (V82.tclEVARS sigma) (f gl) + tclTHEN (Unsafe.tclEVARS sigma) (f gl) with e when catchable_exception e -> let e = Errors.push e in tclZERO e @@ -1032,7 +938,7 @@ module Goal = struct Env.get >>= fun env -> tclEVARMAP >>= fun sigma -> let (gl,sigma) = nf_gmake env sigma self in - tclTHEN (V82.tclEVARS sigma) (tclUNIT gl) + tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl) let gmake env sigma goal = let info = Evd.find sigma goal in @@ -1148,3 +1054,106 @@ let tclLIFT = Proof.lift let tclCHECKINTERRUPT = tclLIFT (NonLogical.make Control.check_for_interrupt) + + + + + +(*** Compatibility layer with <= 8.2 tactics ***) +module V82 = struct + type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma + + let tactic tac = + (* spiwack: we ignore the dependencies between goals here, + expectingly preserving the semantics of <= 8.2 tactics *) + (* spiwack: convenience notations, waiting for ocaml 3.12 *) + let (>>=) = Proof.bind in + Pv.get >>= fun ps -> + try + let tac gl evd = + let glsigma = + tac { Evd.it = gl ; sigma = evd; } in + let sigma = glsigma.Evd.sigma in + let g = glsigma.Evd.it in + ( g, sigma ) + in + (* Old style tactics expect the goals normalized with respect to evars. *) + let (initgoals,initevd) = + Evd.Monad.List.map (fun g s -> GoalV82.nf_evar s g) ps.comb ps.solution + in + let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in + let sgs = List.flatten goalss in + Pv.set { solution = evd; comb = sgs; } + with e when catchable_exception e -> + let e = Errors.push e in + tclZERO e + + + (* normalises the evars in the goals, and stores the result in + solution. *) + let nf_evar_goals = + Pv.modify begin fun ps -> + let map g s = GoalV82.nf_evar s g in + let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in + { solution = evd; comb = goals; } + end + + let has_unresolved_evar pv = + Evd.has_undefined pv.solution + + (* Main function in the implementation of Grab Existential Variables.*) + let grab pv = + let undef = Evd.undefined_map pv.solution in + let goals = List.rev_map fst (Evar.Map.bindings undef) in + { pv with comb = goals } + + + + (* Returns the open goals of the proofview together with the evar_map to + interprete them. *) + let goals { comb = comb ; solution = solution; } = + { Evd.it = comb ; sigma = solution } + + let top_goals initial { solution=solution; } = + let goals = List.map (fun (t,_) -> fst (Term.destEvar t)) initial in + { Evd.it = goals ; sigma=solution; } + + let top_evars initial = + let evars_of_initial (c,_) = + Evar.Set.elements (Evd.evars_of_term c) + in + List.flatten (List.map evars_of_initial initial) + + let instantiate_evar n com pv = + let (evk,_) = + let evl = Evarutil.non_instantiated pv.solution in + let evl = Evar.Map.bindings evl in + if (n <= 0) then + Errors.error "incorrect existential variable index" + else if List.length evl < n then + Errors.error "not so many uninstantiated existential variables" + else + List.nth evl (n-1) + in + { pv with + solution = Evar_refiner.instantiate_pf_com evk com pv.solution } + + let of_tactic t gls = + try + let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in + let (_,final,_) = apply (GoalV82.env gls.Evd.sigma gls.Evd.it) t init in + { Evd.sigma = final.solution ; it = final.comb } + with Proofview_monad.TacticFailure e as src -> + let src = Errors.push src in + let e = Backtrace.app_backtrace ~src ~dst:e in + raise e + + let put_status = Status.put + + let catchable_exception = catchable_exception + + let wrap_exceptions f = + try f () + with e when catchable_exception e -> let e = Errors.push e in tclZERO e + +end diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 7f070d006..cb0df1853 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -307,6 +307,19 @@ val tclTIME : string option -> 'a tactic -> 'a tactic (** [mark_as_unsafe] signals that the current tactic is unsafe. *) val mark_as_unsafe : unit tactic +module Unsafe : sig + + (* Assumes the new evar_map does not change existing goals *) + val tclEVARS : Evd.evar_map -> unit tactic + + (* Assumes the new evar_map might be solving some existing goals *) + val tclEVARSADVANCE : Evd.evar_map -> unit tactic + + (* Set the evar universe context *) + val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic + +end + module Monad : Monad.S with type +'a t = 'a tactic (*** Commands ***) @@ -326,60 +339,6 @@ module Notations : sig end -(*** Compatibility layer with <= 8.2 tactics ***) -module V82 : sig - type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma - val tactic : tac -> unit tactic - - (* normalises the evars in the goals, and stores the result in - solution. *) - val nf_evar_goals : unit tactic - - (* Assumes the new evar_map does not change existing goals *) - val tclEVARS : Evd.evar_map -> unit tactic - - (* Assumes the new evar_map might be solving some existing goals *) - val tclEVARSADVANCE : Evd.evar_map -> unit tactic - - (* Set the evar universe context *) - val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic - - val has_unresolved_evar : proofview -> bool - - (* Main function in the implementation of Grab Existential Variables. - Resets the proofview's goals so that it contains all unresolved evars - (in chronological order of insertion). *) - val grab : proofview -> proofview - - (* Returns the open goals of the proofview together with the evar_map to - interprete them. *) - val goals : proofview -> Evar.t list Evd.sigma - - val top_goals : entry -> proofview -> Evar.t list Evd.sigma - - (* returns the existential variable used to start the proof *) - val top_evars : entry -> Evd.evar list - - (* Implements the Existential command *) - val instantiate_evar : int -> Constrexpr.constr_expr -> proofview -> proofview - - (* Caution: this function loses quite a bit of information. It - should be avoided as much as possible. It should work as - expected for a tactic obtained from {!V82.tactic} though. *) - val of_tactic : 'a tactic -> tac - - (* marks as unsafe if the argument is [false] *) - val put_status : bool -> unit tactic - - (* exception for which it is deemed to be safe to transmute into - tactic failure. *) - val catchable_exception : exn -> bool - - (* transforms every Ocaml (catchable) exception into a failure in - the monad. *) - val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic -end - (* The module goal provides an interface for goal-dependent tactics. *) (* spiwack: there are still parts of the code which depend on proofs/goal.ml. Eventually I'll try to remove it in favour of [Proofview.Goal] *) @@ -506,3 +465,51 @@ end (* [tclLIFT c] includes the non-logical command [c] in a tactic. *) val tclLIFT : 'a NonLogical.t -> 'a tactic + + + + +(*** Compatibility layer with <= 8.2 tactics ***) +module V82 : sig + type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma + val tactic : tac -> unit tactic + + (* normalises the evars in the goals, and stores the result in + solution. *) + val nf_evar_goals : unit tactic + + val has_unresolved_evar : proofview -> bool + + (* Main function in the implementation of Grab Existential Variables. + Resets the proofview's goals so that it contains all unresolved evars + (in chronological order of insertion). *) + val grab : proofview -> proofview + + (* Returns the open goals of the proofview together with the evar_map to + interprete them. *) + val goals : proofview -> Evar.t list Evd.sigma + + val top_goals : entry -> proofview -> Evar.t list Evd.sigma + + (* returns the existential variable used to start the proof *) + val top_evars : entry -> Evd.evar list + + (* Implements the Existential command *) + val instantiate_evar : int -> Constrexpr.constr_expr -> proofview -> proofview + + (* Caution: this function loses quite a bit of information. It + should be avoided as much as possible. It should work as + expected for a tactic obtained from {!V82.tactic} though. *) + val of_tactic : 'a tactic -> tac + + (* marks as unsafe if the argument is [false] *) + val put_status : bool -> unit tactic + + (* exception for which it is deemed to be safe to transmute into + tactic failure. *) + val catchable_exception : exn -> bool + + (* transforms every Ocaml (catchable) exception into a failure in + the monad. *) + val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic +end diff --git a/tactics/auto.ml b/tactics/auto.ml index 39b1ff3c0..18beedf95 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -103,7 +103,7 @@ let exact poly (c,clenv) = in Proofview.Goal.enter begin fun gl -> let sigma = Evd.merge_universe_context (Proofview.Goal.sigma gl) ctx in - Tacticals.New.tclTHEN (Proofview.V82.tclEVARS sigma) (exact_check c') + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (exact_check c') end (* Util *) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index a51c4a962..2be8020a7 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -96,7 +96,7 @@ let one_base general_rewrite_maybe_in tac_main bas = let c' = Vars.subst_univs_level_constr subst c in let sigma = Proofview.Goal.sigma gl in let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in - Tacticals.New.tclTHEN (Proofview.V82.tclEVARS sigma) + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (general_rewrite_maybe_in dir c' tc) ) in let lrul = List.map (fun h -> diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index cb1b7d557..9a241c7ef 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -31,7 +31,7 @@ let absurd c = let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in let t = j.Environ.utj_val in Tacticals.New.tclTHENLIST [ - Proofview.V82.tclEVARS sigma; + Proofview.Unsafe.tclEVARS sigma; elim_type (build_coq_False ()); Simple.apply (mk_absurd_proof t) ] diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index a464b5e8d..93768c10a 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -71,7 +71,7 @@ END TACTIC EXTEND left_with [ "left" "with" bindings(bl) ] -> [ let { Evd.sigma = sigma ; it = bl } = bl in - Proofview.V82.tclEVARS sigma <*> Tactics.left_with_bindings false bl + Proofview.Unsafe.tclEVARS sigma <*> Tactics.left_with_bindings false bl ] END @@ -95,7 +95,7 @@ END TACTIC EXTEND right_with [ "right" "with" bindings(bl) ] -> [ let { Evd.sigma = sigma ; it = bl } = bl in - Proofview.V82.tclEVARS sigma <*> Tactics.right_with_bindings false bl + Proofview.Unsafe.tclEVARS sigma <*> Tactics.right_with_bindings false bl ] END @@ -118,7 +118,7 @@ TACTIC EXTEND constructor let { Evd.sigma = sigma; it = bl } = bl in let i = Tacinterp.interp_int_or_var ist i in let tac c = Tactics.constructor_tac false None i c in - Proofview.V82.tclEVARS sigma <*> tac bl + Proofview.Unsafe.tclEVARS sigma <*> tac bl ] END @@ -142,7 +142,7 @@ TACTIC EXTEND specialize [ "specialize" constr_with_bindings(c) ] -> [ let { Evd.sigma = sigma; it = c } = c in let specialize c = Proofview.V82.tactic (Tactics.specialize c) in - Proofview.V82.tclEVARS sigma <*> specialize c + Proofview.Unsafe.tclEVARS sigma <*> specialize c ] END @@ -163,7 +163,7 @@ END TACTIC EXTEND split_with [ "split" "with" bindings(bl) ] -> [ let { Evd.sigma = sigma ; it = bl } = bl in - Proofview.V82.tclEVARS sigma <*> Tactics.split_with_bindings false [bl] + Proofview.Unsafe.tclEVARS sigma <*> Tactics.split_with_bindings false [bl] ] END diff --git a/tactics/equality.ml b/tactics/equality.ml index 79e852815..425e9f290 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -238,7 +238,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim = let try_clause c = side_tac (tclTHEN - (Proofview.V82.tclEVARS c.evd) + (Proofview.Unsafe.tclEVARS c.evd) (general_elim_clause with_evars frzevars cls c elim)) tac in @@ -348,7 +348,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d let type_of_cls = type_of_clause cls gl in let dep = dep_proof_ok && dep_fun c type_of_cls in let (sigma,elim,effs) = find_elim hdcncl lft2rgt dep cls (Some t) gl in - Proofview.V82.tclEVARS sigma <*> Proofview.tclEFFECTS effs <*> + Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclEFFECTS effs <*> general_elim_clause with_evars frzevars tac cls c t l (match lft2rgt with None -> false | Some b -> b) {elimindex = None; elimbody = (elim,NoBindings); elimrename = None} @@ -925,7 +925,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort = let pf_ty = mkArrow eqn absurd_term in let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in let pf = Clenvtac.clenv_value_cast_meta absurd_clause in - Proofview.V82.tclEVARS sigma <*> + Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclEFFECTS eff <*> tclTHENS (assert_after Anonymous absurd_term) [onLastHypId gen_absurdity; (Proofview.V82.tactic (refine pf))] @@ -954,7 +954,7 @@ let onEquality with_evars tac (c,lbindc) = let eqn = clenv_type eq_clause' in let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in tclTHEN - (Proofview.V82.tclEVARS eq_clause'.evd) + (Proofview.Unsafe.tclEVARS eq_clause'.evd) (tac (eq,eqn,eq_args) eq_clause') end @@ -1308,7 +1308,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = if List.is_empty injectors then Proofview.tclZERO (Errors.UserError ("Equality.inj" , str "Failed to decompose the equality.")) else - Proofview.tclTHEN (Proofview.V82.tclEVARS !evdref) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Proofview.tclBIND (Proofview.Monad.List.map (fun (pf,ty) -> tclTHENS (cut ty) @@ -1482,7 +1482,7 @@ let cutSubstInConcl l2r eqn = let sigma,typ,expected = pf_apply subst_tuple_term gl e1 e2 typ in tclTHENFIRST (tclTHENLIST [ - (Proofview.V82.tclEVARS sigma); + (Proofview.Unsafe.tclEVARS sigma); (Proofview.V82.tactic (change_concl typ)); (* Put in pattern form *) (replace_core onConcl l2r eqn) ]) @@ -1497,7 +1497,7 @@ let cutSubstInHyp l2r eqn id = let sigma,typ,expected = pf_apply subst_tuple_term gl e1 e2 typ in tclTHENFIRST (tclTHENLIST [ - (Proofview.V82.tclEVARS sigma); + (Proofview.Unsafe.tclEVARS sigma); (Proofview.V82.tactic (change_in_hyp None (fun _ s -> s,typ) (id,InHypTypeOnly))); (replace_core (onHyp id) l2r eqn) ]) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 71d766e12..bce768cd4 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -34,12 +34,12 @@ TACTIC EXTEND admit END let replace_in_clause_maybe_by (sigma,c1) c2 cl tac = - Proofview.V82.tclEVARS sigma <*> + Proofview.Unsafe.tclEVARS sigma <*> (replace_in_clause_maybe_by c1 c2 cl) (Option.map Tacinterp.eval_tactic tac) let replace_term dir_opt (sigma,c) cl = - Proofview.V82.tclEVARS sigma <*> + Proofview.Unsafe.tclEVARS sigma <*> (replace_term dir_opt c) cl TACTIC EXTEND replace @@ -202,7 +202,7 @@ END let onSomeWithHoles tac = function | None -> tac None - | Some c -> Proofview.V82.tclEVARS c.sigma <*> tac (Some c.it) + | Some c -> Proofview.Unsafe.tclEVARS c.sigma <*> tac (Some c.it) TACTIC EXTEND contradiction [ "contradiction" constr_with_bindings_opt(c) ] -> @@ -246,7 +246,7 @@ END let rewrite_star clause orient occs (sigma,c) (tac : glob_tactic_expr option) = let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in - Proofview.V82.tclEVARS sigma <*> + Proofview.Unsafe.tclEVARS sigma <*> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true TACTIC EXTEND rewrite_star diff --git a/tactics/inv.ml b/tactics/inv.ml index 457068c6c..62117bff7 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -459,7 +459,7 @@ let raw_inversion inv_kind id status names = in let neqns = List.length realargs in let as_mode = names != None in - tclTHEN (Proofview.V82.tclEVARS sigma) + tclTHEN (Proofview.Unsafe.tclEVARS sigma) (tclTHENS (assert_before Anonymous cut_concl) [case_tac names diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index b55ee7030..ec9a9ff3e 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1478,13 +1478,13 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = match is_hyp, prf with | Some id, Some p -> let tac = Proofview.Refine.refine (fun h -> (h, p)) <*> Proofview.tclNEWGOALS gls in - Proofview.V82.tclEVARS undef <*> + Proofview.Unsafe.tclEVARS undef <*> assert_replacing id newt tac | Some id, None -> - Proofview.V82.tclEVARS undef <*> + Proofview.Unsafe.tclEVARS undef <*> convert_hyp_no_check (id, None, newt) | None, Some p -> - Proofview.V82.tclEVARS undef <*> + Proofview.Unsafe.tclEVARS undef <*> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let make sigma = @@ -1494,7 +1494,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = Proofview.Refine.refine make <*> Proofview.tclNEWGOALS gls end | None, None -> - Proofview.V82.tclEVARS undef <*> + Proofview.Unsafe.tclEVARS undef <*> convert_concl_no_check newt DEFAULTcast in let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f7c3c922f..8f516802d 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -598,7 +598,7 @@ let new_interp_constr ist c k = let open Proofview in Proofview.Goal.enter begin fun gl -> let (sigma, c) = interp_constr ist (Goal.env gl) (Goal.sigma gl) c in - Proofview.tclTHEN (Proofview.V82.tclEVARS sigma) (k c) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k c) end let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = @@ -1135,7 +1135,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let concl = Proofview.Goal.concl gl in let goal = Proofview.Goal.goal gl in let (sigma, arg) = interp_genarg ist env sigma concl goal x in - Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return arg) + Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return arg) end | _ as tag -> (** Special treatment. TODO: use generic handler *) Ftactic.nf_enter begin fun gl -> @@ -1154,17 +1154,17 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let (sigma,v) = Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl in - Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return v) + Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v) | OpenConstrArgType -> let (sigma,v) = Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl in - Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return v) + Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v) | ConstrMayEvalArgType -> let (sigma,c_interp) = interp_constr_may_eval ist env sigma (out_gen (glbwit wit_constr_may_eval) x) in - Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return (Value.of_constr c_interp)) + Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp)) | ListArgType ConstrArgType -> let wit = glbwit (wit_list wit_constr) in let (sigma,l_interp) = Tacmach.New.of_old begin fun gl -> @@ -1173,7 +1173,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with (out_gen wit x) (project gl) end gl in - Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return (in_gen (topwit (wit_list wit_genarg)) l_interp)) + Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (in_gen (topwit (wit_list wit_genarg)) l_interp)) | ListArgType VarArgType -> let wit = glbwit (wit_list wit_var) in Ftactic.return ( @@ -1208,7 +1208,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with else let goal = Proofview.Goal.goal gl in let (newsigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} x in - Ftactic.(lift (Proofview.V82.tclEVARS newsigma) <*> return v) + Ftactic.(lift (Proofview.Unsafe.tclEVARS newsigma) <*> return v) | _ -> assert false end in @@ -1254,7 +1254,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Evd.MonadR.List.map_right (fun a sigma -> interp_genarg ist env sigma concl goal a) l goal_sigma in - Proofview.V82.tclEVARS sigma <*> + Proofview.Unsafe.tclEVARS sigma <*> catch_error_tac trace (tac args ist) end @@ -1293,7 +1293,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = let sigma = Proofview.Goal.sigma gl in let goal = Proofview.Goal.goal gl in let (sigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} arg in - Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return v) + Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v) end | Reference r -> interp_ltac_reference dloc false ist r | ConstrMayEval c -> @@ -1301,7 +1301,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in - Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return (Value.of_constr c_interp)) + Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp)) end | UConstr c -> Ftactic.enter begin fun gl -> @@ -1335,7 +1335,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = let (sigma,c_interp) = Pretyping.understand_ltac constr_flags env sigma vars WithoutTypeConstraint term in - Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return (Value.of_constr c_interp)) + Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp)) end | TacNumgoals -> Ftactic.lift begin @@ -1688,7 +1688,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in - Proofview.V82.tclEVARS sigma <*> Tactics.intros_patterns l' + Proofview.Unsafe.tclEVARS sigma <*> Tactics.intros_patterns l' end | TacIntroMove (ido,hto) -> Proofview.Goal.enter begin fun gl -> @@ -1784,7 +1784,7 @@ and interp_atomic ist tac : unit Proofview.tactic = in let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in let tac = Option.map (interp_tactic ist) t in - Proofview.V82.tclEVARS sigma <*> Tactics.forward b tac ipat c + Proofview.Unsafe.tclEVARS sigma <*> Tactics.forward b tac ipat c end | TacGeneralize cl -> let tac arg = Proofview.V82.tactic (Tactics.Simple.generalize_gen arg) in @@ -1792,7 +1792,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in - Proofview.V82.tclEVARS sigma <*> tac cl + Proofview.Unsafe.tclEVARS sigma <*> tac cl end | TacGeneralizeDep c -> (new_interp_constr ist c) @@ -1814,7 +1814,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let with_eq = if b then None else Some (true,id) in Tactics.letin_tac with_eq na c None cl in - Proofview.V82.tclEVARS sigma <*> + Proofview.Unsafe.tclEVARS sigma <*> let_tac b (interp_fresh_name ist env sigma na) c_interp clp eqpat else (* We try to keep the pattern structure as much as possible *) @@ -1992,7 +1992,7 @@ and interp_atomic ist tac : unit Proofview.tactic = in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let sigma,ids = interp_or_and_intro_pattern_option ist env sigma ids in - Proofview.V82.tclEVARS sigma <*> Inv.dinv k c_interp ids dqhyps + Proofview.Unsafe.tclEVARS sigma <*> Inv.dinv k c_interp ids dqhyps end | TacInversion (NonDepInversion (k,idl,ids),hyp) -> Proofview.Goal.enter begin fun gl -> @@ -2001,7 +2001,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let hyps = interp_hyp_list ist env sigma idl in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let sigma, ids = interp_or_and_intro_pattern_option ist env sigma ids in - Proofview.V82.tclEVARS sigma <*> Inv.inv_clause k ids hyps dqhyps + Proofview.Unsafe.tclEVARS sigma <*> Inv.inv_clause k ids hyps dqhyps end | TacInversion (InversionUsing (c,idl),hyp) -> Proofview.Goal.enter begin fun gl -> @@ -2010,7 +2010,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let (sigma,c_interp) = interp_constr ist env sigma c in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let hyps = interp_hyp_list ist env sigma idl in - Proofview.V82.tclEVARS sigma <*> + Proofview.Unsafe.tclEVARS sigma <*> Leminv.lemInv_clause dqhyps c_interp hyps diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 600ad86ef..2a21c53ab 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -494,7 +494,7 @@ module New = struct else tclUNIT () in - Proofview.V82.tclEVARS sigma <*> tac x <*> check_evars_if + Proofview.Unsafe.tclEVARS sigma <*> tac x <*> check_evars_if let tclTIMEOUT n t = Proofview.tclOR @@ -684,7 +684,7 @@ module New = struct let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let (sigma, c) = Evd.fresh_global env sigma ref in - Proofview.V82.tclEVARS sigma <*> (tac c) + Proofview.Unsafe.tclEVARS sigma <*> (tac c) end end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ea40fe4b9..83a3f2604 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -132,7 +132,7 @@ let convert_concl ?(check=true) ty k = sigma end else sigma in Tacticals.New.tclTHEN - (Proofview.V82.tclEVARS sigma) + (Proofview.Unsafe.tclEVARS sigma) (Proofview.Refine.refine ~unsafe:true (fun sigma -> let (sigma,x) = Evarutil.new_evar env sigma ~principal:true ty in (sigma, if k == DEFAULTcast then x else mkCast(x,k,conclty)))) @@ -155,7 +155,7 @@ let convert_gen pb x y = Proofview.Goal.enter begin fun gl -> try let sigma = Tacmach.New.pf_apply Evd.conversion gl pb x y in - Proofview.V82.tclEVARS sigma + Proofview.Unsafe.tclEVARS sigma with (* Reduction.NotConvertible *) _ -> (** FIXME: Sometimes an anomaly is raised from conversion *) Tacticals.New.tclFAIL 0 (str "Not convertible") @@ -909,7 +909,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) let naming = NamingMustBe (dloc,targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN - (Proofview.V82.tclEVARS clenv.evd) + (Proofview.Unsafe.tclEVARS clenv.evd) (if sidecond_first then Tacticals.New.tclTHENFIRST (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac @@ -1051,7 +1051,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = build_case_analysis_scheme env sigma mind true sort else build_case_analysis_scheme_default env sigma mind sort in - Tacticals.New.tclTHEN (Proofview.V82.tclEVARS sigma) + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (general_elim with_evars clear_flag (c,lbindc) {elimindex = None; elimbody = (elim,NoBindings); elimrename = Some (false, constructors_nrealdecls (fst mind))}) @@ -1090,7 +1090,7 @@ let default_elim with_evars clear_flag (c,_ as cx) = Proofview.tclORELSE (Proofview.Goal.enter begin fun gl -> let evd, elim = find_eliminator c gl in - Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evd) + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd) (general_elim with_evars clear_flag cx elim) end) begin function @@ -1266,7 +1266,7 @@ let solve_remaining_apply_goals = if Typeclasses.is_class_type sigma concl then let evd', c' = Typeclasses.resolve_one_typeclass env sigma concl in Tacticals.New.tclTHEN - (Proofview.V82.tclEVARS evd') + (Proofview.Unsafe.tclEVARS evd') (Proofview.V82.tactic (refine_no_check c')) else Proofview.tclUNIT () with Not_found -> Proofview.tclUNIT () @@ -1460,7 +1460,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma, c = f env sigma in - Proofview.V82.tclEVARS sigma <*> + Proofview.Unsafe.tclEVARS sigma <*> (apply_in_once sidecond_first with_delta with_destruct with_evars naming id (clear_flag,(loc,c)) tac) end @@ -1518,7 +1518,7 @@ let exact_check c = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma, ct = Typing.e_type_of env sigma c in - Proofview.V82.tclEVARS sigma <*> + Proofview.Unsafe.tclEVARS sigma <*> Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c) end @@ -1550,7 +1550,7 @@ let assumption = infer_conv env sigma t concl in if is_same_type then - (Proofview.V82.tclEVARS sigma) <*> + (Proofview.Unsafe.tclEVARS sigma) <*> Proofview.Refine.refine ~unsafe:true (fun h -> (h, mkVar id)) else arec gl only_eq rest in @@ -1582,7 +1582,7 @@ let check_is_type env ty msg = let evdref = ref sigma in try let _ = Typing.sort_of env evdref ty in - Proofview.V82.tclEVARS !evdref + Proofview.Unsafe.tclEVARS !evdref with e when Errors.noncritical e -> msg e @@ -1595,7 +1595,7 @@ let check_decl env (_, c, ty) msg = | None -> () | Some c -> Typing.check env evdref c ty in - Proofview.V82.tclEVARS !evdref + Proofview.Unsafe.tclEVARS !evdref with e when Errors.noncritical e -> msg e @@ -1739,7 +1739,7 @@ let constructor_tac with_evars expctdnumopt i lbind = let apply_tac = general_apply true false with_evars None (dloc,(cons,lbind)) in (Tacticals.New.tclTHENLIST - [Proofview.V82.tclEVARS sigma; + [Proofview.Unsafe.tclEVARS sigma; convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) end @@ -1993,7 +1993,7 @@ and intro_pattern_action loc b style pat thin tac id = match pat with let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let sigma,c = f env sigma in - Proofview.V82.tclEVARS sigma <*> + Proofview.Unsafe.tclEVARS sigma <*> (Tacticals.New.tclTHENFIRST (* Skip the side conditions of the apply *) (apply_in_once false true true true naming id @@ -2143,11 +2143,11 @@ let letin_tac_gen with_eq abs ty = | None -> (Proofview.Goal.sigma gl, mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in Tacticals.New.tclTHEN - (Proofview.V82.tclEVARUNIVCONTEXT ctx) + (Proofview.Unsafe.tclEVARUNIVCONTEXT ctx) (Proofview.Goal.nf_enter (fun gl -> let (sigma,newcl,eq_tac) = eq_tac gl in Tacticals.New.tclTHENLIST - [ Proofview.V82.tclEVARS sigma; + [ Proofview.Unsafe.tclEVARS sigma; convert_concl_no_check newcl DEFAULTcast; intro_gen (NamingMustBe (dloc,id)) (decode_hyp lastlhyp) true false; Tacticals.New.tclMAP convert_hyp_no_check depdecls; @@ -2314,7 +2314,7 @@ let new_generalize_gen_let lconstr = generalize_goal_gen env ids i o t cl, args) 0 lconstr ((concl, sigma), []) in - Proofview.V82.tclEVARS sigma <*> + Proofview.Unsafe.tclEVARS sigma <*> Proofview.Refine.refine begin fun sigma -> let (sigma, ev) = Evarutil.new_evar env sigma newcl in (sigma, (applist (ev, args))) @@ -3497,7 +3497,7 @@ let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names t Proofview.Goal.nf_enter begin fun gl -> let (sigma, isrec, elim, indsign) = get_eliminator elim gl in let names = compute_induction_names (Array.length indsign) names in - Tacticals.New.tclTHEN (Proofview.V82.tclEVARS sigma) + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) ((if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) (Tacticals.New.tclTHEN (induct_tac elim) @@ -3611,7 +3611,7 @@ let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbin Proofview.Goal.nf_enter begin fun gl -> let sigma, elim_info = find_induction_type isrec elim hyp0 gl in Tacticals.New.tclTHENLIST - [Proofview.V82.tclEVARS sigma; (atomize_param_of_ind elim_info hyp0); + [Proofview.Unsafe.tclEVARS sigma; (atomize_param_of_ind elim_info hyp0); (induction_from_context isrec with_evars elim_info (hyp0,lbind) names inhyps)] end @@ -3631,7 +3631,7 @@ let induction_without_atomization isrec with_evars elim names lid = if not (Int.equal nlid awaited_nargs) then Tacticals.New.tclZEROMSG (str"Not the right number of induction arguments.") else - Proofview.tclTHEN (Proofview.V82.tclEVARS sigma) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (induction_from_context_l with_evars elim_info lid names) end @@ -3855,7 +3855,7 @@ let elim_type t = Proofview.Goal.enter begin fun gl -> let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in - Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evd) (elim_scheme_type elimc t) + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t) end let case_type t = @@ -3864,7 +3864,7 @@ let case_type t = let evd, elimc = Tacmach.New.pf_apply build_case_analysis_scheme_default gl ind (Tacticals.New.elimination_sort_of_goal gl) in - Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evd) (elim_scheme_type elimc t) + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t) end @@ -4125,7 +4125,7 @@ let abstract_subproof id gk tac = Entries.(snd (Future.force const.const_entry_body)) in let args = List.rev (instance_from_named_context sign) in let solve = - Proofview.V82.tclEVARS evd <*> + Proofview.Unsafe.tclEVARS evd <*> Proofview.tclEFFECTS effs <*> new_exact_no_check (applist (lem, args)) in @@ -4168,7 +4168,7 @@ let unify ?(state=full_transparent_state) x y = subterm_unify_flags = { core_flags with modulo_delta = empty_transparent_state } } in let evd = w_unify (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) Reduction.CONV ~flags x y - in Proofview.V82.tclEVARS evd + in Proofview.Unsafe.tclEVARS evd with e when Errors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Not unifiable") end |