diff options
-rw-r--r-- | plugins/btauto/refl_btauto.ml | 9 | ||||
-rw-r--r-- | plugins/cc/cctac.ml | 38 | ||||
-rw-r--r-- | plugins/fourier/fourierR.ml | 5 | ||||
-rw-r--r-- | plugins/micromega/coq_micromega.ml | 24 | ||||
-rw-r--r-- | plugins/omega/coq_omega.ml | 29 | ||||
-rw-r--r-- | plugins/quote/quote.ml | 9 | ||||
-rw-r--r-- | plugins/setoid_ring/newring.ml | 9 | ||||
-rw-r--r-- | proofs/clenvtac.ml | 10 | ||||
-rw-r--r-- | proofs/proofview.ml | 17 | ||||
-rw-r--r-- | proofs/proofview.mli | 9 | ||||
-rw-r--r-- | proofs/tactic_debug.ml | 5 | ||||
-rw-r--r-- | tactics/auto.ml | 41 | ||||
-rw-r--r-- | tactics/autorewrite.ml | 8 | ||||
-rw-r--r-- | tactics/class_tactics.ml | 15 | ||||
-rw-r--r-- | tactics/contradiction.ml | 16 | ||||
-rw-r--r-- | tactics/eauto.ml4 | 30 | ||||
-rw-r--r-- | tactics/elim.ml | 16 | ||||
-rw-r--r-- | tactics/eqdecide.ml | 21 | ||||
-rw-r--r-- | tactics/equality.ml | 92 | ||||
-rw-r--r-- | tactics/extratactics.ml4 | 44 | ||||
-rw-r--r-- | tactics/inv.ml | 22 | ||||
-rw-r--r-- | tactics/leminv.ml | 5 | ||||
-rw-r--r-- | tactics/rewrite.ml | 17 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 116 | ||||
-rw-r--r-- | tactics/tacticals.ml | 53 | ||||
-rw-r--r-- | tactics/tactics.ml | 244 | ||||
-rw-r--r-- | tactics/tauto.ml4 | 5 | ||||
-rw-r--r-- | toplevel/auto_ind_decl.ml | 40 |
28 files changed, 483 insertions, 466 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 57268a9cf..5a49fc8f4 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -1,3 +1,4 @@ +open Proofview.Notations let contrib_name = "btauto" @@ -216,7 +217,7 @@ module Btauto = struct Tacticals.tclFAIL 0 msg gl let try_unification env = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let eq = Lazy.force eq in let t = decomp_term concl in @@ -228,10 +229,10 @@ module Btauto = struct | _ -> let msg = str "Btauto: Internal error" in Tacticals.New.tclFAIL 0 msg - end + end } let tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let eq = Lazy.force eq in let bool = Lazy.force Bool.typ in @@ -255,6 +256,6 @@ module Btauto = struct | _ -> let msg = str "Cannot recognize a boolean equality" in Tacticals.New.tclFAIL 0 msg - end + end } end diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 068cb25cf..35178aa1e 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -22,6 +22,7 @@ open Ccproof open Pp open Errors open Util +open Proofview.Notations let reference dir s = lazy (Coqlib.gen_reference "CC" dir s) @@ -254,13 +255,13 @@ let new_app_global f args k = let new_refine c = Proofview.V82.tactic (refine c) let assert_before n c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let evm, _ = Tacmach.New.pf_apply type_of gl c in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c) - end + end } let rec proof_tac p : unit Proofview.tactic = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of t = Tacmach.New.pf_unsafe_type_of gl t in try (* type_of can raise exceptions *) match p.p_rule with @@ -325,10 +326,10 @@ let rec proof_tac p : unit Proofview.tactic = app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e - end + end } let refute_tac c t1 t2 p = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let intype = Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl @@ -338,14 +339,14 @@ let refute_tac c t1 t2 p = let false_t=mkApp (c,[|mkVar hid|]) in Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; simplest_elim false_t] - end + end } let refine_exact_check c gl = let evm, _ = pf_apply type_of gl c in Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl let convert_to_goal_tac c t1 t2 p = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let sort = Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl @@ -357,20 +358,20 @@ let convert_to_goal_tac c t1 t2 p = let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in Tacticals.New.tclTHENS (neweq (assert_before (Name e))) [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)] - end + end } let convert_to_hyp_tac c1 t1 c2 t2 p = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let tt2=constr_of_term t2 in let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in let false_t=mkApp (c2,[|mkVar h|]) in Tacticals.New.tclTHENS (assert_before (Name h) tt2) [convert_to_goal_tac c1 t1 t2 p; simplest_elim false_t] - end + end } let discriminate_tac (cstr,u as cstru) p = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in let intype = Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl @@ -399,7 +400,7 @@ let discriminate_tac (cstr,u as cstru) p = 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 + end } (* wrap everything *) @@ -411,7 +412,7 @@ let build_term_to_complete uf meta pac = applistc (mkConstructU cinfo.ci_constr) all_args let cc_tactic depth additionnal_terms = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> Coqlib.check_required_library Coqlib.logic_module_name; let _ = debug (Pp.str "Reading subgoal ...") in let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in @@ -462,7 +463,7 @@ let cc_tactic depth additionnal_terms = convert_to_goal_tac id ta tb p | HeqnH (ida,idb) -> convert_to_hyp_tac ida ta idb tb p - end + end } let cc_fail gls = errorlabstrm "Congruence" (Pp.str "congruence failed.") @@ -485,8 +486,7 @@ let congruence_tac depth l = let mk_eq f c1 c2 k = Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> - Proofview.Goal.enter begin - fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let open Tacmach.New in let evm, ty = pf_apply type_of gl c1 in let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in @@ -494,10 +494,10 @@ let mk_eq f c1 c2 k = let evm, _ = type_of (pf_env gl) evm term in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k term) - end) + end }) let f_equal = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let cut_eq c1 c2 = try (* type_of can raise an exception *) @@ -523,4 +523,4 @@ let f_equal = | Type_errors.TypeError _ -> Proofview.tclUNIT () | e -> Proofview.tclZERO ~info e end - end + end } diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 7a56cd665..e5c9b2707 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -19,6 +19,7 @@ open Globnames open Tacmach open Fourier open Contradiction +open Proofview.Notations (****************************************************************************** Opérations sur les combinaisons linéaires affines. @@ -462,7 +463,7 @@ exception GoalDone (* Résolution d'inéquations linéaires dans R *) let rec fourier () = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; let goal = strip_outer_cast concl in @@ -622,7 +623,7 @@ let rec fourier () = (* ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *) !tac (* ((tclABSTRACT None !tac) gl) *) - end + end } ;; (* diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index ef1169342..a0e61623c 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -20,6 +20,7 @@ open Pp open Mutils open Proofview open Goptions +open Proofview.Notations (** * Debug flag @@ -1444,8 +1445,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in let vm = dump_varmap (spec.typ) env in (* todo : directly generate the proof term - or generalize before conversion? *) - Proofview.Goal.nf_enter - begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> Tacticals.New.tclTHENLIST [ Tactics.change_concl @@ -1462,7 +1462,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* Tactics.new_generalize env ; Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] - end + end } (** @@ -1707,9 +1707,7 @@ let micromega_gen (normalise:'cst atom -> 'cst mc_cnf) unsat deduce spec prover = - Proofview.Goal.nf_enter - begin - fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in try @@ -1735,7 +1733,7 @@ let micromega_gen ^ "the use of a specialized external tool called csdp. \n\n" ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) - end + end } let micromega_gen parse_arith (negate:'cst atom -> 'cst mc_cnf) @@ -1756,9 +1754,7 @@ let micromega_order_changer cert env ff = let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in let vm = dump_varmap (typ) env in - Proofview.Goal.nf_enter - begin - fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> Tacticals.New.tclTHENLIST [ (Tactics.change_concl @@ -1774,7 +1770,7 @@ let micromega_order_changer cert env ff = Tactics.new_generalize env ; Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] - end + end } let micromega_genr prover = @@ -1790,9 +1786,7 @@ let micromega_genr prover = proof_typ = Lazy.force coq_QWitness ; dump_proof = dump_psatz coq_Q dump_q } in - Proofview.Goal.nf_enter - begin - fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in try @@ -1822,7 +1816,7 @@ let micromega_genr prover = ^ "the use of a specialized external tool called csdp. \n\n" ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) - end + end } let micromega_genr prover = (micromega_genr prover) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index aac9a7d31..976ab949c 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -27,6 +27,7 @@ open Globnames open Nametab open Contradiction open Misctypes +open Proofview.Notations module OmegaSolver = Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -34,9 +35,9 @@ open OmegaSolver (* Added by JCF, 09/03/98 *) let elim_id id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> simplest_elim (Tacmach.New.pf_global id gl) - end + end } let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl let timing timer_name f arg = f arg @@ -1416,7 +1417,7 @@ let reintroduce id = open Proofview.Notations let coq_omega = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> clear_constr_tables (); let hyps_types = Tacmach.New.pf_hyps_types gl in let destructure_omega = Tacmach.New.of_old destructure_omega gl in @@ -1464,12 +1465,12 @@ let coq_omega = Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path) with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system") end - end + end } let coq_omega = coq_omega let nat_inject = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in let rec explore p t : unit Proofview.tactic = try match destructurate_term t with @@ -1603,7 +1604,7 @@ let nat_inject = in let hyps_types = Tacmach.New.pf_hyps_types gl in loop (List.rev hyps_types) - end + end } let dec_binop = function | Zne -> coq_dec_Zne @@ -1673,22 +1674,22 @@ let onClearedName id tac = (* so renaming may be necessary *) Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTRY (clear [id]))) - (Proofview.Goal.nf_enter begin fun gl -> + (Proofview.Goal.nf_enter { enter = begin fun gl -> let id = Tacmach.New.of_old (fresh_id [] id) gl in Tacticals.New.tclTHEN (introduction id) (tac id) - end) + end }) let onClearedName2 id tac = Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTRY (clear [id]))) - (Proofview.Goal.nf_enter begin fun gl -> + (Proofview.Goal.nf_enter { enter = begin fun gl -> let id1 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) gl in let id2 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) gl in Tacticals.New.tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] - end) + end }) let destructure_hyps = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in let decidability = Tacmach.New.of_old decidability gl in let pf_nf = Tacmach.New.of_old pf_nf gl in @@ -1828,10 +1829,10 @@ let destructure_hyps = in let hyps = Proofview.Goal.hyps gl in loop hyps - end + end } let destructure_goal = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let decidability = Tacmach.New.of_old decidability gl in let rec loop t = @@ -1855,7 +1856,7 @@ let destructure_goal = Tacticals.New.tclTHEN goal_tac destructure_hyps in (loop concl) - end + end } let destructure_goal = destructure_goal diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 2a2ef30fb..8d60b8ba2 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -109,6 +109,7 @@ open Pattern open Patternops open Constr_matching open Tacmach +open Proofview.Notations (*i*) (*s First, we need to access some Coq constants @@ -446,7 +447,7 @@ let quote_terms ivs lc = yet. *) let quote f lid = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let f = Tacmach.New.pf_global f gl in let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in let ivs = compute_ivs f cl gl in @@ -459,10 +460,10 @@ let quote f lid = match ivs.variable_lhs with | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast - end + end } let gen_quote cont c f lid = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let f = Tacmach.New.pf_global f gl in let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in let ivs = compute_ivs f cl gl in @@ -474,7 +475,7 @@ let gen_quote cont c f lid = match ivs.variable_lhs with | None -> cont (mkApp (f, [| p |])) | Some _ -> cont (mkApp (f, [| vm; p |])) - end + end } (*i diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 942ca15a5..8ff4230e8 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -31,6 +31,7 @@ open Decl_kinds open Entries open Misctypes open Newring_ast +open Proofview.Notations (****************************************************************************) (* controlled reduction *) @@ -747,7 +748,7 @@ let ltac_ring_structure e = lemma1;lemma2;pretac;posttac] let ring_lookup (f:glob_tactic_expr) lH rl t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in try (* find_ring_strucure can raise an exception *) @@ -759,7 +760,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t = let ring = ltac_ring_structure e in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl])) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e - end + end } (***********************************************************************) @@ -1019,7 +1020,7 @@ let ltac_field_structure e = field_simpl_eq_in_ok;cond_ok;pretac;posttac] let field_lookup (f:glob_tactic_expr) lH rl t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in try @@ -1031,4 +1032,4 @@ let field_lookup (f:glob_tactic_expr) lH rl t = let field = ltac_field_structure e in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl])) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e - end + end } diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index f54d4c447..65bd32536 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -16,7 +16,7 @@ open Logic open Reduction open Tacmach open Clenv - +open Proofview.Notations (* This function put casts around metavariables whose type could not be * infered by the refiner, that is head of applications, predicates and @@ -83,10 +83,10 @@ open Unification let dft = default_unify_flags let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let clenv gl = clenv_unique_resolver ~flags clenv gl in clenv_refine with_evars ~with_classes (Tacmach.New.of_old clenv (Proofview.Goal.assume gl)) - end + end } (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en particulier ne semblent pas vérifier que des instances différentes @@ -118,7 +118,7 @@ let fail_quick_unif_flags = { (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) let unify ?(flags=fail_quick_unif_flags) m = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Tacmach.New.pf_env gl in let n = Tacmach.New.pf_nf_concl gl in let evd = clear_metas (Proofview.Goal.sigma gl) in @@ -126,4 +126,4 @@ let unify ?(flags=fail_quick_unif_flags) m = let evd' = w_unify env evd CONV ~flags m n in Proofview.Unsafe.tclEVARSADVANCE evd' with e when Errors.noncritical e -> Proofview.tclZERO e - end + end } diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 7edbef57b..b8a58daeb 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -915,6 +915,9 @@ module Goal = struct self : Evar.t ; (* for compatibility with old-style definitions *) } + type 'a enter = + { enter : 'a t -> unit tactic } + let assume (gl : 'a t) = (gl :> [ `NF ] t) let env { env=env } = env @@ -944,7 +947,7 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try let (gl, sigma) = nf_gmake env sigma goal in - tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl)) + tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f.enter gl)) with e when catchable_exception e -> let (e, info) = Errors.push e in tclZERO ~info e @@ -962,7 +965,7 @@ module Goal = struct gmake_with info env sigma goal let enter f = - let f gl = InfoL.tag (Info.DBranch) (f gl) in + let f gl = InfoL.tag (Info.DBranch) (f.enter gl) in InfoL.tag (Info.Dispatch) begin iter_goal begin fun goal -> Env.get >>= fun env -> @@ -1054,7 +1057,7 @@ struct let (pr_constrv,pr_constr) = Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") () - let refine ?(unsafe = true) f = Goal.enter begin fun gl -> + let refine ?(unsafe = true) f = Goal.enter { Goal.enter = begin fun gl -> let sigma = Goal.sigma gl in let env = Goal.env gl in let concl = Goal.concl gl in @@ -1091,7 +1094,7 @@ struct let open Proof in InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >> Pv.set { solution = sigma; comb; } - end + end } (** Useful definitions *) @@ -1103,7 +1106,7 @@ struct in evd , j'.Environ.uj_val - let refine_casted ?unsafe f = Goal.enter begin fun gl -> + let refine_casted ?unsafe f = Goal.enter { Goal.enter = begin fun gl -> let concl = Goal.concl gl in let env = Goal.env gl in let f = { run = fun h -> @@ -1112,7 +1115,7 @@ struct Sigma (c, Sigma.Unsafe.of_evar_map sigma, p) } in refine ?unsafe f - end + end } end @@ -1254,6 +1257,8 @@ module Notations = struct let (>>=) = tclBIND let (<*>) = tclTHEN let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) + type 'a enter = 'a Goal.enter = + { enter : 'a Goal.t -> unit tactic } type 'a s_enter = 'a Goal.s_enter = { s_enter : 'r. 'a Goal.t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma } end diff --git a/proofs/proofview.mli b/proofs/proofview.mli index a94610af4..1616782e5 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -445,14 +445,17 @@ module Goal : sig normalised. *) val raw_concl : 'a t -> Term.constr + type 'a enter = + { enter : 'a t -> unit tactic } + (** [nf_enter t] applies the goal-dependent tactic [t] in each goal independently, in the manner of {!tclINDEPENDENT} except that the current goal is also given as an argument to [t]. The goal is normalised with respect to evars. *) - val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic + val nf_enter : [ `NF ] enter -> unit tactic (** Like {!nf_enter}, but does not normalize the goal beforehand. *) - val enter : ([ `LZ ] t -> unit tactic) -> unit tactic + val enter : [ `LZ ] enter -> unit tactic type 'a s_enter = { s_enter : 'r. 'a t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma } @@ -592,6 +595,8 @@ module Notations : sig (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *) val (<+>) : 'a tactic -> 'a tactic -> 'a tactic + type 'a enter = 'a Goal.enter = + { enter : 'a Goal.t -> unit tactic } type 'a s_enter = 'a Goal.s_enter = { s_enter : 'r. 'a Goal.t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma } end diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 6d6215c52..fb23a28fe 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -12,6 +12,7 @@ open Pp open Tacexpr open Termops open Nameops +open Proofview.Notations let (prtac, tactic_printer) = Hook.make () let (prmatchpatt, match_pattern_printer) = Hook.make () @@ -47,10 +48,10 @@ let db_pr_goal gl = str" " ++ pc) ++ fnl () let db_pr_goal = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let pg = db_pr_goal gl in Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg)) - end + end } (* Prints the commands *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 686d4b471..4e4eafe4e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -96,11 +96,11 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = in clenv, c let unify_resolve poly flags ((c : raw_hint), clenv) = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let clenv, c = connect_hint_clenv poly c clenv gl in let clenv = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv gl) gl in Clenvtac.clenv_refine false clenv - end + end } let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h @@ -151,11 +151,12 @@ let conclPattern concl pat tac = with Constr_matching.PatternMatchingFailure -> Tacticals.New.tclZEROMSG (str "conclPattern") in - Proofview.Goal.enter (fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in constr_bindings env sigma >>= fun constr_bindings -> - Hook.get forward_interp_tactic constr_bindings tac) + Hook.get forward_interp_tactic constr_bindings tac + end } (***********************************************************) (** A debugging / verbosity framework for trivial and auto *) @@ -320,7 +321,7 @@ let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption let rec trivial_fail_db dbg mod_delta db_list local_db = let intro_tac = Tacticals.New.tclTHEN (dbg_intro dbg) - ( Proofview.Goal.enter begin fun gl -> + ( Proofview.Goal.enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let nf c = Evarutil.nf_evar sigma c in @@ -329,15 +330,15 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = let hintl = make_resolve_hyp env sigma hyp in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list env sigma hintl local_db) - end) + end }) in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let concl = Tacmach.New.pf_nf_concl gl in Tacticals.New.tclFIRST ((dbg_assumption dbg)::intro_tac:: (List.map Tacticals.New.tclCOMPLETE (trivial_resolve dbg mod_delta db_list local_db concl))) - end + end } and my_find_search_nodelta db_list local_db hdc concl = List.map (fun hint -> (None,hint)) @@ -414,7 +415,7 @@ and trivial_resolve dbg mod_delta db_list local_db cl = "nocore" amongst the databases. *) let trivial ?(debug=Off) lems dbnames = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let db_list = make_db_list dbnames in @@ -422,10 +423,10 @@ let trivial ?(debug=Off) lems dbnames = let hints = make_local_hint_db env sigma false lems in tclTRY_dbg d (trivial_fail_db d false db_list hints) - end + end } let full_trivial ?(debug=Off) lems = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let db_list = current_pure_db () in @@ -433,7 +434,7 @@ let full_trivial ?(debug=Off) lems = let hints = make_local_hint_db env sigma false lems in tclTRY_dbg d (trivial_fail_db d false db_list hints) - end + end } let gen_trivial ?(debug=Off) lems = function | None -> full_trivial ~debug lems @@ -466,10 +467,10 @@ let extend_local_db decl db gl = let intro_register dbg kont db = Tacticals.New.tclTHEN (dbg_intro dbg) - (Proofview.Goal.enter begin fun gl -> + (Proofview.Goal.enter { enter = begin fun gl -> let extend_local_db decl db = extend_local_db decl db gl in Tacticals.New.onLastDecl (fun decl -> kont (extend_local_db decl db)) - end) + end }) (* n is the max depth of search *) (* local_db contains the local Hypotheses *) @@ -482,14 +483,14 @@ let search d n mod_delta db_list local_db = if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else Tacticals.New.tclORELSE0 (dbg_assumption d) (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db) - ( Proofview.Goal.enter begin fun gl -> + ( Proofview.Goal.enter { enter = begin fun gl -> let concl = Tacmach.New.pf_nf_concl gl in let d' = incr_dbg d in Tacticals.New.tclFIRST (List.map (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db)) (possible_resolve d mod_delta db_list local_db concl)) - end)) + end })) end [] in search d n local_db @@ -497,7 +498,7 @@ let search d n mod_delta db_list local_db = let default_search_depth = ref 5 let delta_auto debug mod_delta n lems dbnames = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let db_list = make_db_list dbnames in @@ -505,7 +506,7 @@ let delta_auto debug mod_delta n lems dbnames = let hints = make_local_hint_db env sigma false lems in tclTRY_dbg d (search d n mod_delta db_list hints) - end + end } let delta_auto = if Flags.profile then @@ -520,7 +521,7 @@ let new_auto ?(debug=Off) n = delta_auto debug true n let default_auto = auto !default_search_depth [] [] let delta_full_auto ?(debug=Off) mod_delta n lems = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let db_list = current_pure_db () in @@ -528,7 +529,7 @@ let delta_full_auto ?(debug=Off) mod_delta n lems = let hints = make_local_hint_db env sigma false lems in tclTRY_dbg d (search d n mod_delta db_list hints) - end + end } let full_auto ?(debug=Off) n = delta_full_auto ~debug false n let new_full_auto ?(debug=Off) n = delta_full_auto ~debug true n diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 2ecba176a..43a8d7f06 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -123,7 +123,7 @@ let autorewrite ?(conds=Naive) tac_main lbas = (Proofview.tclUNIT()) lbas)) let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> (* let's check at once if id exists (to raise the appropriate error) *) let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in let general_rewrite_in id = @@ -166,7 +166,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = (List.fold_left (fun tac bas -> Tacticals.New.tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) (Proofview.tclUNIT()) lbas))) idl - end + end } let autorewrite_in ?(conds=Naive) id = autorewrite_multi_in ~conds [id] @@ -191,10 +191,10 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = | None -> (* try to rewrite in all hypothesis (except maybe the rewritten one) *) - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let ids = Tacmach.New.pf_ids_of_hyps gl in try_do_hyps (fun id -> id) ids - end) + end }) let auto_multi_rewrite ?(conds=Naive) = gen_auto_multi_rewrite conds (Proofview.tclUNIT()) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 83b1202b7..9c22beba2 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -140,17 +140,17 @@ let rec eq_constr_mod_evars x y = | _, _ -> compare_constr eq_constr_mod_evars x y let progress_evars t = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let check = - Proofview.Goal.nf_enter begin fun gl' -> + Proofview.Goal.nf_enter { enter = begin fun gl' -> let newconcl = Proofview.Goal.concl gl' in if eq_constr_mod_evars concl newconcl then Tacticals.New.tclFAIL 0 (str"No progress made (modulo evars)") else Proofview.tclUNIT () - end + end } in t <*> check - end + end } let e_give_exact flags poly (c,clenv) gl = @@ -188,10 +188,11 @@ let clenv_of_prods poly nprods (c, clenv) gl = else None let with_prods nprods poly (c, clenv) f = - Proofview.Goal.nf_enter (fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> match clenv_of_prods poly nprods (c, clenv) gl with | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses") - | Some clenv' -> f (c, clenv') gl) + | Some clenv' -> f (c, clenv') gl + end } (** Hack to properly solve dependent evars that are typeclasses *) @@ -901,5 +902,5 @@ let autoapply c i gl = (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in let cty = pf_unsafe_type_of gl c in let ce = mk_clenv_from gl (c,cty) in - let tac = unify_e_resolve false flags ((c,cty,Univ.ContextSet.empty),ce) in + let tac = { enter = fun gl -> unify_e_resolve false flags ((c,cty,Univ.ContextSet.empty),ce) gl } in Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 7deb4baf6..34886d74d 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -48,13 +48,13 @@ let filter_hyp f tac = | [] -> Proofview.tclZERO Not_found | (id,_,t)::rest when f t -> tac id | _::rest -> seek rest in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in seek hyps - end + end } let contradiction_context = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let rec seek_neg l = match l with @@ -67,11 +67,11 @@ let contradiction_context = else match kind_of_term typ with | Prod (na,t,u) when is_empty_type u -> (Proofview.tclORELSE - (Proofview.Goal.enter begin fun gl -> + (Proofview.Goal.enter { enter = begin fun gl -> let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in filter_hyp (fun typ -> is_conv_leq typ t) (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|]))) - end) + end }) begin function (e, info) -> match e with | Not_found -> seek_neg rest | e -> Proofview.tclZERO ~info e @@ -80,7 +80,7 @@ let contradiction_context = in let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in seek_neg hyps - end + end } let is_negation_of env sigma typ t = match kind_of_term (whd_betadeltaiota env sigma t) with @@ -90,7 +90,7 @@ let is_negation_of env sigma typ t = | _ -> false let contradiction_term (c,lbind as cl) = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in @@ -113,7 +113,7 @@ let contradiction_term (c,lbind as cl) = | Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.") | e -> Proofview.tclZERO ~info e end - end + end } let contradiction = function | None -> Tacticals.New.tclTHEN intros contradiction_context diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index d0fd4b078..08502e0cc 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -28,26 +28,27 @@ open Misctypes open Locus open Locusops open Hints +open Proofview.Notations DECLARE PLUGIN "eauto" let eauto_unif_flags = auto_flags_of_state full_transparent_state let e_give_exact ?(flags=eauto_unif_flags) c = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let t1 = Tacmach.New.pf_unsafe_type_of gl c in let t2 = Tacmach.New.pf_concl gl in if occur_existential t1 || occur_existential t2 then Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c)) else exact_check c - end + end } let assumption id = e_give_exact (mkVar id) let e_assumption = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> Tacticals.New.tclFIRST (List.map assumption (Tacmach.New.pf_ids_of_hyps gl)) - end + end } TACTIC EXTEND eassumption | [ "eassumption" ] -> [ e_assumption ] @@ -58,10 +59,10 @@ TACTIC EXTEND eexact END let registered_e_assumption = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id)) (Tacmach.New.pf_ids_of_hyps gl)) - end + end } (************************************************************************) (* PROLOG tactic *) @@ -126,15 +127,14 @@ open Unification let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l) let unify_e_resolve poly flags (c,clenv) = - Proofview.Goal.nf_enter begin - fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let clenv', c = connect_hint_clenv poly c clenv gl in Proofview.V82.tactic (fun gls -> let clenv' = clenv_unique_resolver ~flags clenv' gls in tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls) - end + end } let hintmap_of hdc concl = match hdc with @@ -152,19 +152,19 @@ let e_exact poly flags (c,clenv) = in e_give_exact (* ~flags *) (Vars.subst_univs_level_constr subst c) let rec e_trivial_fail_db db_list local_db = - let next = Proofview.Goal.nf_enter begin fun gl -> + let next = Proofview.Goal.nf_enter { enter = begin fun gl -> let d = Tacmach.New.pf_last_hyp gl in let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) d in e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) hintl local_db) - end in - Proofview.Goal.enter begin fun gl -> + end } in + Proofview.Goal.enter { enter = begin fun gl -> let tacl = registered_e_assumption :: (Tacticals.New.tclTHEN Tactics.intro next) :: (List.map fst (e_trivial_resolve db_list local_db (Tacmach.New.pf_nf_concl gl))) in Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl) - end + end } and e_my_find_search db_list local_db hdc concl = let hint_of_db = hintmap_of hdc concl in @@ -567,7 +567,7 @@ let unfold_head env (ids, csts) c = in aux c let autounfold_one db cl = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let st = @@ -586,7 +586,7 @@ let autounfold_one db cl = | Some hyp -> change_in_hyp None (make_change_arg c') hyp | None -> convert_concl_no_check c' DEFAULTcast else Tacticals.New.tclFAIL 0 (str "Nothing to unfold") - end + end } (* Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts *) (* (Id.Set.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) *) diff --git a/tactics/elim.ml b/tactics/elim.ml index 4841d2c25..27e96637d 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -84,7 +84,7 @@ let tmphyp_name = Id.of_string "_TmpHyp" let up_to_delta = ref false (* true *) let general_decompose recognizer c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let type_of = pf_unsafe_type_of gl in let typc = type_of c in tclTHENS (cut typc) @@ -93,7 +93,7 @@ let general_decompose recognizer c = (ifOnHyp recognizer (general_decompose_aux recognizer) (fun id -> Proofview.V82.tactic (clear [id])))); Proofview.V82.tactic (exact_no_check c) ] - end + end } let head_in indl t gl = let env = Proofview.Goal.env gl in @@ -107,10 +107,10 @@ let head_in indl t gl = with Not_found -> false let decompose_these c l = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let indl = List.map (fun x -> x, Univ.Instance.empty) l in general_decompose (fun (_,t) -> head_in indl t gl) c - end + end } let decompose_and c = general_decompose @@ -138,7 +138,7 @@ let induction_trailer abs_i abs_j bargs = (tclDO (abs_j - abs_i) intro) (onLastHypId (fun id -> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let idty = pf_unsafe_type_of gl (mkVar id) in let fvty = global_vars (pf_env gl) idty in let possible_bring_hyps = @@ -156,11 +156,11 @@ let induction_trailer abs_i abs_j bargs = (tclTHENLIST [bring_hyps hyps; tclTRY (Proofview.V82.tactic (clear ids)); simple_elimination (mkVar id)]) - end + end } )) let double_ind h1 h2 = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let abs_i = of_old (depth_of_quantified_hypothesis true h1) gl in let abs_j = of_old (depth_of_quantified_hypothesis true h2) gl in let abs = @@ -173,7 +173,7 @@ let double_ind h1 h2 = (fun id -> elimination_then (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id)))) - end + end } let h_double_induction = double_ind diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 4fb76bb82..74e5e036a 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -27,6 +27,7 @@ open Constr_matching open Hipattern open Tacmach.New open Coqlib +open Proofview.Notations (* This file containts the implementation of the tactics ``Decide Equality'' and ``Compare''. They can be used to decide the @@ -146,7 +147,7 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with intros_reflexivity; ] | a1 :: largs, a2 :: rargs -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let rectype = pf_unsafe_type_of gl a1 in let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in @@ -154,13 +155,13 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto] else [diseqCase hyps eqonleft;eqCase tac;default_auto] in (tclTHENS (elim_type decide) subtacs) - end + end } | _ -> invalid_arg "List.fold_right2" let solveEqBranch rectype = Proofview.tclORELSE begin - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let concl = pf_nf_concl gl in match_eqdec concl >>= fun (eqonleft,op,lhs,rhs,_) -> let (mib,mip) = Global.lookup_inductive rectype in @@ -169,7 +170,7 @@ let solveEqBranch rectype = let rargs = getargs rhs and largs = getargs lhs in solveArg [] eqonleft op largs rargs - end + end } end begin function (e, info) -> match e with | PatternMatchingFailure -> Tacticals.New.tclZEROMSG (Pp.str"Unexpected conclusion!") @@ -185,7 +186,7 @@ let hd_app c = match kind_of_term c with let decideGralEquality = Proofview.tclORELSE begin - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let concl = pf_nf_concl gl in match_eqdec concl >>= fun (eqonleft,_,c1,c2,typ) -> let headtyp = hd_app (pf_compute gl typ) in @@ -196,7 +197,7 @@ let decideGralEquality = (tclTHEN (mkBranches c1 c2) (tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype))) - end + end } end begin function (e, info) -> match e with | PatternMatchingFailure -> @@ -207,20 +208,20 @@ let decideGralEquality = let decideEqualityGoal = tclTHEN intros decideGralEquality let decideEquality rectype = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let decide = mkGenDecideEqGoal rectype gl in (tclTHENS (cut decide) [default_auto;decideEqualityGoal]) - end + end } (* The tactic Compare *) let compare c1 c2 = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let rectype = pf_unsafe_type_of gl c1 in let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in (tclTHENS (cut decide) [(tclTHEN intro (tclTHEN (onLastHyp simplest_case) clear_last)); decideEquality rectype]) - end + end } diff --git a/tactics/equality.ml b/tactics/equality.ml index fdc77be2f..e8f88fca1 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -207,10 +207,10 @@ let rewrite_conv_closed_unif_flags = { } let rewrite_elim with_evars frzevars cls c e = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_conv_closed_unif_flags c in general_elim_clause with_evars flags cls c e - end + end } (* Ad hoc asymmetric general_elim_clause *) let general_elim_clause with_evars frzevars cls rew elim = @@ -245,7 +245,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim = (general_elim_clause with_evars frzevars cls c elim)) tac in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let instantiate_lemma concl = if not all then instantiate_lemma gl c t l l2r concl else instantiate_lemma_all frzevars gl c t l l2r concl @@ -257,7 +257,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim = let cs = instantiate_lemma typ in if firstonly then tclFIRST (List.map try_clause cs) else tclMAP try_clause cs - end + end } (* The next function decides in particular whether to try a regular rewrite or a generalized rewrite. @@ -383,7 +383,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac if occs != AllOccurrences then ( rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac) else - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let ctype = get_type_of env sigma c in @@ -411,7 +411,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac | None -> Proofview.tclZERO ~info e (* error "The provided term does not end with an equality or a declared rewrite relation." *) end - end + end } let general_rewrite_ebindings = general_rewrite_ebindings_clause None @@ -473,9 +473,9 @@ let general_rewrite_clause l2r with_evars ?tac c cl = let ids_of_hyps = pf_ids_of_hyps gl in Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> do_hyps_atleastonce (ids gl) - end + end } in if cl.concl_occs == NoOccurrences then do_hyps else tclIFTHENTRYELSEMUST @@ -483,7 +483,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl = do_hyps let apply_special_clear_request clear_flag f = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in try @@ -491,17 +491,17 @@ let apply_special_clear_request clear_flag f = apply_clear_request clear_flag (use_clear_hyp_by_default ()) c with e when catchable_exception e -> tclIDTAC - end + end } let general_multi_rewrite with_evars l cl tac = let do1 l2r f = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let (c, sigma) = run_delayed env sigma f in tclWITHHOLES with_evars (general_rewrite_clause l2r with_evars ?tac c cl) sigma - end + end } in let rec doN l2r c = function | Precisely n when n <= 0 -> Proofview.tclUNIT () @@ -564,7 +564,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = | None -> Proofview.tclUNIT () | Some tac -> tclCOMPLETE tac in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let get_type_of = pf_apply get_type_of gl in let t1 = get_type_of c1 and t2 = get_type_of c2 in @@ -590,7 +590,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = tclTHEN (apply sym) assumption; try_prove_eq ]))) - end + end } let replace c1 c2 = replace_using_leibniz onConcl c2 c1 false false None @@ -873,7 +873,7 @@ let rec build_discriminator env sigma dirn c sort = function *) let gen_absurdity id = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in let hyp_typ = pf_nf_evar gl hyp_typ in if is_empty_type hyp_typ @@ -881,7 +881,7 @@ let gen_absurdity id = simplest_elim (mkVar id) else tclZEROMSG (str "Not the negation of an equality.") - end + end } (* Precondition: eq is leibniz equality @@ -937,7 +937,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort = let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in match find_positions env sigma t1 t2 with @@ -946,10 +946,10 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = | Inl (cpath, (_,dirn), _) -> let sort = pf_apply get_type_of gl concl in discr_positions env sigma u eq_clause cpath dirn sort - end + end } let onEquality with_evars tac (c,lbindc) = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of = pf_unsafe_type_of gl in let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in let t = type_of c in @@ -961,10 +961,10 @@ let onEquality with_evars tac (c,lbindc) = tclTHEN (Proofview.Unsafe.tclEVARS eq_clause'.evd) (tac (eq,eqn,eq_args) eq_clause') - end + end } let onNegatedEquality with_evars tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let ccl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in @@ -975,7 +975,7 @@ let onNegatedEquality with_evars tac = onEquality with_evars tac (mkVar id,NoBindings))) | _ -> tclZEROMSG (str "Not a negated primitive equality.") - end + end } let discrSimpleClause with_evars = function | None -> onNegatedEquality with_evars discrEq @@ -1244,7 +1244,7 @@ let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined") let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k) let inject_if_homogenous_dependent_pair ty = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> try let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in (* fetch the informations of the pair *) @@ -1282,7 +1282,7 @@ let inject_if_homogenous_dependent_pair ty = ])] with Exit -> Proofview.tclUNIT () - end + end } (* Given t1=t2 Inj calculates the whd normal forms of t1 and t2 and it expands then only when the whdnf has a constructor of an inductive type @@ -1374,7 +1374,7 @@ let injConcl = injClause None false None let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id))) let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let sort = pf_apply get_type_of gl (Proofview.Goal.concl gl) in let sigma = clause.evd in let env = Proofview.Goal.env gl in @@ -1386,7 +1386,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause = | Inr posns -> inject_at_positions env sigma true u clause posns (ntac (clenv_value clause)) - end + end } let dEqThen with_evars ntac = function | None -> onNegatedEquality with_evars (decompEqThen (ntac None)) @@ -1397,10 +1397,10 @@ let dEq with_evars = (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)) let intro_decompe_eq tac data cl = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let cl = pf_apply make_clenv_binding gl cl NoBindings in decompEqThen (fun _ -> tac) data cl - end + end } let _ = declare_intro_decomp_eq intro_decompe_eq @@ -1500,7 +1500,7 @@ let cutSubstInConcl l2r eqn = end } let cutSubstInHyp l2r eqn id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in let typ = pf_get_hyp_typ id gl in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in @@ -1512,7 +1512,7 @@ let cutSubstInHyp l2r eqn id = (replace_core (onHyp id) l2r eqn) ]) (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly)) - end + end } let try_rewrite tac = Proofview.tclORELSE tac begin function (e, info) -> match e with @@ -1534,11 +1534,11 @@ let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id) let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None let substClause l2r c cls = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let eq = pf_apply get_type_of gl c in tclTHENS (cutSubstClause l2r eq cls) [Proofview.tclUNIT (); Proofview.V82.tactic (exact_no_check c)] - end + end } let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls) let rewriteInHyp l2r c id = rewriteClause l2r c (Some id) @@ -1564,7 +1564,7 @@ user = raise user error specific to rewrite (* Substitutions tactics (JCF) *) let unfold_body x = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> (** We normalize the given hypothesis immediately. *) let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in let (_, xval, _) = Context.lookup_named x hyps in @@ -1581,7 +1581,7 @@ let unfold_body x = let reductc = Proofview.V82.tactic (fun gl -> reduct_in_concl (rfun, DEFAULTcast) gl) in tclTHENLIST [tclMAP reducth hl; reductc] end - end + end } let restrict_to_eq_and_identity eq = (* compatibility *) if not (is_global glob_eq eq) && @@ -1604,7 +1604,7 @@ let is_eq_x gl x (id,_,c) = erase hyp and x; proceed by generalizing all dep hyps *) let subst_one dep_proof_ok x (hyp,rhs,dir) = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in @@ -1630,13 +1630,13 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = else [Proofview.tclUNIT ()]) @ [tclTRY (clear [x; hyp])]) - end + end } (* Look for an hypothesis hyp of the form "x=rhs" or "rhs=x", rewrite it everywhere, and erase hyp and x; proceed by generalizing all dep hyps *) let subst_one_var dep_proof_ok x = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let (_,xval,_) = pf_get_hyp x gl in (* If x has a body, simply replace x with body and clear x *) @@ -1655,7 +1655,7 @@ let subst_one_var dep_proof_ok x = str".") with FoundHyp res -> res in subst_one dep_proof_ok x res - end + end } let subst_gen dep_proof_ok ids = tclTHEN Proofview.V82.nf_evar_goals (tclMAP (subst_one_var dep_proof_ok) ids) @@ -1715,7 +1715,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = (* Second step: treat equations *) let process hyp = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let find_eq_data_decompose = find_eq_data_decompose gl in let (_,_,c) = pf_get_hyp hyp gl in @@ -1729,19 +1729,19 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = subst_one flags.rewrite_dependent_proof y' (hyp,x,false) | _ -> Proofview.tclUNIT () - end + end } in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let ids = find_equations gl in tclMAP process ids - end + end } else (* Old implementation, not able to manage configurations like a=b, a=t, or situations like "a = S b, b = S a", or also accidentally unfolding let-ins *) - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let find_eq_data_decompose = find_eq_data_decompose gl in let test (_,c) = try @@ -1758,7 +1758,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let ids = List.map_filter test hyps in let ids = List.uniquize ids in subst_gen flags.rewrite_dependent_proof ids - end + end } (* Rewrite the first assumption for which a condition holds and gives the direction of the rewrite *) @@ -1794,10 +1794,10 @@ let rewrite_assumption_cond cond_eq_term cl = with | Failure _ | UserError _ -> arec rest gl end in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let hyps = Proofview.Goal.hyps gl in arec hyps gl - end + end } (* Generalize "subst x" to substitution of subterm appearing as an equation in the context, but not clearing the hypothesis *) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 7b754636f..fa13234a6 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -22,6 +22,7 @@ open Evd open Equality open Misctypes open Sigma.Notations +open Proofview.Notations DECLARE PLUGIN "extratactics" @@ -346,7 +347,7 @@ END (* Refine *) let refine_tac {Glob_term.closure=closure;term=term} = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let flags = Pretyping.all_no_fail_flags in @@ -362,7 +363,7 @@ let refine_tac {Glob_term.closure=closure;term=term} = Sigma.Unsafe.of_pair (c, sigma) end } in Tactics.New.refine ~unsafe:false update - end + end } TACTIC EXTEND refine [ "refine" uconstr(c) ] -> [ refine_tac c ] @@ -662,7 +663,7 @@ END *) let hget_evar n = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let concl = Proofview.Goal.concl gl in let evl = evar_list concl in @@ -672,7 +673,7 @@ let hget_evar n = let ev = List.nth evl (n-1) in let ev_type = existential_type sigma ev in change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl)) - end + end } TACTIC EXTEND hget_evar | [ "hget_evar" int_or_var(n) ] -> [ hget_evar (out_arg n) ] @@ -691,12 +692,12 @@ END exception Found of unit Proofview.tactic let rewrite_except h = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let hyps = Tacmach.New.pf_ids_of_hyps gl in Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false)) hyps - end + end } let refl_equal = @@ -710,27 +711,27 @@ let refl_equal = should be replaced by a call to the tactic but I don't know how to call it before it is defined. *) let mkCaseEq a : unit Proofview.tactic = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in Tacticals.New.tclTHENLIST [Proofview.V82.tactic (Tactics.Simple.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]); - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in change_concl (snd (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl)) - end; + end }; simplest_case a] - end + end } let case_eq_intros_rewrite x = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let n = nb_prod (Proofview.Goal.concl gl) in (* Pp.msgnl (Printer.pr_lconstr x); *) Tacticals.New.tclTHENLIST [ mkCaseEq x; - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let hyps = Tacmach.New.pf_ids_of_hyps gl in let n' = nb_prod concl in @@ -739,9 +740,9 @@ let case_eq_intros_rewrite x = Tacticals.New.tclDO (n'-n-1) intro; introduction h; rewrite_except h] - end + end } ] - end + end } let rec find_a_destructable_match t = match kind_of_term t with @@ -761,15 +762,15 @@ let destauto t = with Found tac -> tac let destauto_in id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in (* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) (* Pp.msgnl (Printer.pr_lconstr (ctype)); *) destauto ctype - end + end } TACTIC EXTEND destauto -| [ "destauto" ] -> [ Proofview.Goal.nf_enter (fun gl -> destauto (Proofview.Goal.concl gl)) ] +| [ "destauto" ] -> [ Proofview.Goal.nf_enter { enter = begin fun gl -> destauto (Proofview.Goal.concl gl) end } ] | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ] END @@ -777,10 +778,11 @@ END (* ********************************************************************* *) let eq_constr x y = - Proofview.Goal.enter (fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let evd = Proofview.Goal.sigma gl in if Evarutil.eq_constr_univs_test evd evd x y then Proofview.tclUNIT () - else Tacticals.New.tclFAIL 0 (str "Not equal")) + else Tacticals.New.tclFAIL 0 (str "Not equal") + end } TACTIC EXTEND constr_eq | [ "constr_eq" constr(x) constr(y) ] -> [ eq_constr x y ] @@ -981,14 +983,14 @@ TACTIC EXTEND guard END let decompose l c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let to_ind c = if isInd c then Univ.out_punivs (destInd c) else error "not an inductive type" in let l = List.map to_ind l in Elim.h_decompose l c - end + end } TACTIC EXTEND decompose | [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ] diff --git a/tactics/inv.ml b/tactics/inv.ml index f326e2479..a9fa52e92 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -270,14 +270,14 @@ Nota: with Inversion_clear, only four useless hypotheses let generalizeRewriteIntros as_mode tac depids id = Proofview.tclENV >>= fun env -> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let dids = dependent_hyps env id depids gl in let reintros = if as_mode then intros_replacing else intros_possibly_replacing in (tclTHENLIST [bring_hyps dids; tac; (* may actually fail to replace if dependent in a previous eq *) reintros (ids_of_named_context dids)]) - end + end } let error_too_many_names pats = let loc = Loc.join_loc (fst (List.hd pats)) (fst (List.last pats)) in @@ -339,7 +339,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC)) in let substHypIfVariable tac id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> (** We only look at the type of hypothesis "id" *) let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in @@ -347,7 +347,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1 | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2 | _ -> tac id - end + end } in let deq_trailer id clear_flag _ neqns = assert (clear_flag == None); @@ -374,7 +374,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = id let nLastDecls i tac = - Proofview.Goal.nf_enter (fun gl -> tac (nLastDecls gl i)) + Proofview.Goal.nf_enter { enter = begin fun gl -> tac (nLastDecls gl i) end } (* Introduction of the equations on arguments othin: discriminates Simple Inversion, Inversion and Inversion_clear @@ -382,7 +382,7 @@ let nLastDecls i tac = Some thin: the equations are rewritten, and cleared if thin is true *) let rewrite_equations as_mode othin neqns names ba = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in let first_eq = ref MoveLast in let avoid = if as_mode then List.map pi1 nodepids else [] in @@ -415,7 +415,7 @@ let rewrite_equations as_mode othin neqns names ba = [tclDO neqns intro; bring_hyps nodepids; clear (ids_of_named_context nodepids)]) - end + end } let interp_inversion_kind = function | SimpleInversion -> None @@ -514,12 +514,12 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id) * back to their places in the hyp-list. *) let invIn k names ids id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let hyps = List.map (fun id -> pf_get_hyp id gl) ids in let concl = Proofview.Goal.concl gl in let nb_prod_init = nb_prod concl in let intros_replace_ids = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let concl = pf_nf_concl gl in let nb_of_new_hyp = nb_prod concl - (List.length hyps + nb_prod_init) @@ -528,7 +528,7 @@ let invIn k names ids id = intros_replacing ids else tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids) - end + end } in Proofview.tclORELSE (tclTHENLIST @@ -536,7 +536,7 @@ let invIn k names ids id = inversion k NoDep names id; intros_replace_ids]) (wrap_inv_error id) - end + end } let invIn_gen k names idl = try_intros_until (invIn k names idl) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 42d22bc3c..04a78dc57 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -27,6 +27,7 @@ open Declare open Tacticals.New open Tactics open Decl_kinds +open Proofview.Notations let no_inductive_inconstr env sigma constr = (str "Cannot recognize an inductive predicate in " ++ @@ -268,7 +269,7 @@ let lemInv id c gls = let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id let lemInvIn id c ids = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let hyps = List.map (fun id -> pf_get_hyp id gl) ids in let intros_replace_ids = let concl = Proofview.Goal.concl gl in @@ -280,7 +281,7 @@ let lemInvIn id c ids = in ((tclTHEN (tclTHEN (bring_hyps hyps) (Proofview.V82.tactic (lemInv id c))) (intros_replace_ids))) - end + end } let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 7e0182137..2667fa7ff 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -35,6 +35,7 @@ open Environ open Termops open Libnames open Sigma.Notations +open Proofview.Notations (** Typeclass-based generalized rewriting. *) @@ -1501,7 +1502,7 @@ let rec insert_dependent env decl accu hyps = match hyps with insert_dependent env decl (ndecl :: accu) rem let assert_replacing id newt tac = - let prf = Proofview.Goal.nf_enter begin fun gl -> + let prf = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let ctx = Environ.named_context env in @@ -1518,7 +1519,7 @@ let assert_replacing id newt tac = let (e, _) = destEvar ev in Sigma (mkEvar (e, Array.map_of_list map nc), sigma, p +> q) end } - end in + end } in Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac) let newfail n s = @@ -1544,14 +1545,14 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = convert_hyp_no_check (id, None, newt) | None, Some p -> Proofview.Unsafe.tclEVARS undef <*> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let make = { run = begin fun sigma -> let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma newt in Sigma (mkApp (p, [| ev |]), sigma, q) end } in Proofview.Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls - end + end } | None, None -> Proofview.Unsafe.tclEVARS undef <*> convert_concl_no_check newt DEFAULTcast @@ -1562,7 +1563,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = | None -> Proofview.tclUNIT () | Some id -> Proofview.V82.tactic (Tactics.reduct_in_hyp beta_red (id, InHyp)) in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in @@ -1590,7 +1591,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = with | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) -> raise (RewriteFailure (Himsg.explain_pretype_error env evd e)) - end + end } let tactic_init_setoid () = try init_setoid (); tclIDTAC @@ -2037,7 +2038,7 @@ let not_declared env ty rel = str ty ++ str" relation. Maybe you need to require the Setoid library") let setoid_proof ty fn fallback = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let concl = Proofview.Goal.concl gl in @@ -2066,7 +2067,7 @@ let setoid_proof ty fn fallback = | e' -> Proofview.tclZERO ~info e' end end - end + end } let tac_open ((evm,_), c) tac = Proofview.V82.tactic diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 895064951..1ea19bce0 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -632,10 +632,10 @@ let pf_interp_constr ist gl = let new_interp_constr ist c k = let open Proofview in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (sigma, c) = interp_constr ist (Goal.env gl) (Goal.sigma gl) c in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k c) - end + end } let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let try_expand_ltac_var sigma x = @@ -1172,9 +1172,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) end | TacAbstract (tac,ido) -> - Proofview.Goal.nf_enter begin fun gl -> Tactics.tclABSTRACT + Proofview.Goal.nf_enter { enter = begin fun gl -> Tactics.tclABSTRACT (Option.map (Tacmach.New.of_old (pf_interp_ident ist) gl) ido) (interp_tactic ist tac) - end + end } | TacThen (t1,t) -> Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t) | TacDispatch tl -> @@ -1350,7 +1350,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacML (loc,opn,l) -> let trace = push_trace (loc,LtacMLCall tac) ist in let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let goal_sigma = Proofview.Goal.sigma gl in let concl = Proofview.Goal.concl gl in @@ -1364,7 +1364,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let name () = Pptactic.pr_tactic env (TacML(loc,opn,args)) in Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist)) - end + end } and force_vrec ist v : typed_generic_argument Ftactic.t = let v = Value.normalize v in @@ -1803,7 +1803,7 @@ and interp_atomic ist tac : unit Proofview.tactic = match tac with (* Basic tactics *) | TacIntroPattern l -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> 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 @@ -1813,9 +1813,9 @@ and interp_atomic ist tac : unit Proofview.tactic = (* spiwack: print uninterpreted, not sure if it is the expected behaviour. *) (Tactics.intros_patterns l')) sigma - end + end } | TacIntroMove (ido,hto) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let mloc = interp_move_location ist env sigma hto in @@ -1823,7 +1823,7 @@ and interp_atomic ist tac : unit Proofview.tactic = name_atomic ~env (TacIntroMove(ido,mloc)) (Tactics.intro_move ido mloc) - end + end } | TacExact c -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<exact>") begin @@ -1838,7 +1838,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacApply (a,ev,cb,cl) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<apply>") begin - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let l = List.map (fun (k,c) -> @@ -1851,10 +1851,10 @@ and interp_atomic ist tac : unit Proofview.tactic = let sigma,(clear,id,cl) = interp_in_hyp_as ist env sigma cl in sigma, Tactics.apply_delayed_in a ev clear id l cl in Tacticals.New.tclWITHHOLES ev tac sigma - end + end } end | TacElim (ev,(keep,cb),cbo) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in @@ -1864,9 +1864,9 @@ and interp_atomic ist tac : unit Proofview.tactic = name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac in Tacticals.New.tclWITHHOLES ev named_tac sigma - end + end } | TacCase (ev,(keep,cb)) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in @@ -1875,16 +1875,16 @@ and interp_atomic ist tac : unit Proofview.tactic = name_atomic ~env (TacCase(ev,(keep,cb))) tac in Tacticals.New.tclWITHHOLES ev named_tac sigma - end + end } | TacFix (idopt,n) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let idopt = Option.map (interp_ident ist env sigma) idopt in name_atomic ~env (TacFix(idopt,n)) (Proofview.V82.tactic (Tactics.fix idopt n)) - end + end } | TacMutualFix (id,n,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin @@ -1903,14 +1903,14 @@ and interp_atomic ist tac : unit Proofview.tactic = end end | TacCofix idopt -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let idopt = Option.map (interp_ident ist env sigma) idopt in name_atomic ~env (TacCofix (idopt)) (Proofview.V82.tactic (Tactics.cofix idopt)) - end + end } | TacMutualCofix (id,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin @@ -1929,7 +1929,7 @@ and interp_atomic ist tac : unit Proofview.tactic = end end | TacAssert (b,t,ipat,c) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let (sigma,c) = @@ -1941,9 +1941,9 @@ and interp_atomic ist tac : unit Proofview.tactic = (name_atomic ~env (TacAssert(b,t,ipat,c)) (Tactics.forward b tac ipat' c)) sigma - end + end } | TacGeneralize cl -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> 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 @@ -1951,7 +1951,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (name_atomic ~env (TacGeneralize cl) (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl))) sigma - end + end } | TacGeneralizeDep c -> (new_interp_constr ist c) (fun c -> name_atomic (* spiwack: probably needs a goal environment *) @@ -1960,7 +1960,7 @@ and interp_atomic ist tac : unit Proofview.tactic = ) | TacLetTac (na,c,clp,b,eqpat) -> Proofview.V82.nf_evar_goals <*> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let clp = interp_clause ist env sigma clp in @@ -1993,7 +1993,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*) (let_pat_tac b (interp_name ist env sigma na) ((sigma,sigma'),c) clp eqpat) sigma') - end + end } (* Automation tactics *) | TacTrivial (debug,lems,l) -> @@ -2003,7 +2003,7 @@ and interp_atomic ist tac : unit Proofview.tactic = ++strbrk"does not print traces anymore." ++ spc() ++strbrk"Use \"Info 1 trivial\", instead.") end; - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let lems = interp_auto_lemmas ist env sigma lems in @@ -2012,7 +2012,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (Auto.h_trivial ~debug lems (Option.map (List.map (interp_hint_base ist)) l)) - end + end } | TacAuto (debug,n,lems,l) -> begin if debug == Tacexpr.Info then msg_warning @@ -2020,7 +2020,7 @@ and interp_atomic ist tac : unit Proofview.tactic = ++strbrk"does not print traces anymore." ++ spc() ++strbrk"Use \"Info 1 auto\", instead.") end; - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let lems = interp_auto_lemmas ist env sigma lems in @@ -2029,14 +2029,14 @@ and interp_atomic ist tac : unit Proofview.tactic = (Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n) lems (Option.map (List.map (interp_hint_base ist)) l)) - end + end } (* Derived basic tactics *) | TacInductionDestruct (isrec,ev,(l,el)) -> (* spiwack: some unknown part of destruct needs the goal to be prenormalised. *) Proofview.V82.nf_evar_goals <*> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma,l = @@ -2060,7 +2060,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Tactics.induction_destruct isrec ev (l,el))) - end + end } | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in @@ -2069,7 +2069,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (Elim.h_double_induction h1 h2) (* Context management *) | TacClear (b,l) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Tacmach.New.pf_env gl in let sigma = Proofview.Goal.sigma gl in let l = interp_hyp_list ist env sigma l in @@ -2078,16 +2078,16 @@ and interp_atomic ist tac : unit Proofview.tactic = (* spiwack: until the tactic is in the monad *) let tac = Proofview.V82.tactic (fun gl -> Tactics.clear l gl) in Proofview.Trace.name_tactic (fun () -> Pp.str"<clear>") tac - end + end } | TacClearBody l -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Tacmach.New.pf_env gl in let sigma = Proofview.Goal.sigma gl in let l = interp_hyp_list ist env sigma l in name_atomic ~env (TacClearBody l) (Tactics.clear_body l) - end + end } | TacMove (id1,id2) -> Proofview.V82.tactic begin fun gl -> Tactics.move_hyp (interp_hyp ist (pf_env gl) (project gl) id1) @@ -2095,7 +2095,7 @@ and interp_atomic ist tac : unit Proofview.tactic = gl end | TacRename l -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Tacmach.New.pf_env gl in let sigma = Proofview.Goal.sigma gl in let l = @@ -2106,11 +2106,11 @@ and interp_atomic ist tac : unit Proofview.tactic = name_atomic ~env (TacRename l) (Tactics.rename_hyp l) - end + end } (* Constructors *) | TacSplit (ev,bll) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in @@ -2119,7 +2119,7 @@ and interp_atomic ist tac : unit Proofview.tactic = name_atomic ~env (TacSplit (ev, bll)) tac in Tacticals.New.tclWITHHOLES ev named_tac sigma - end + end } (* Conversion *) | TacReduce (r,cl) -> (* spiwack: until the tactic is in the monad *) @@ -2163,7 +2163,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin Proofview.V82.nf_evar_goals <*> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in Proofview.V82.tactic begin fun gl -> @@ -2182,23 +2182,23 @@ and interp_atomic ist tac : unit Proofview.tactic = (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)) { gl with sigma = sigma } end - end + end } end (* Equivalence relations *) | TacSymmetry c -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let cl = interp_clause ist env sigma c in name_atomic ~env (TacSymmetry cl) (Tactics.intros_symmetry cl) - end + end } (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let l' = List.map (fun (b,m,(keep,c)) -> let f = { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in @@ -2215,9 +2215,9 @@ and interp_atomic ist tac : unit Proofview.tactic = (Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by), Equality.Naive) by)) - end + end } | TacInversion (DepInversion (k,c,ids),hyp) -> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let (sigma,c_interp) = @@ -2235,9 +2235,9 @@ and interp_atomic ist tac : unit Proofview.tactic = (name_atomic ~env (TacInversion(DepInversion(k,c_interp,ids),dqhyps)) (Inv.dinv k c_interp ids_interp dqhyps)) sigma - end + end } | TacInversion (NonDepInversion (k,idl,ids),hyp) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let hyps = interp_hyp_list ist env sigma idl in @@ -2247,9 +2247,9 @@ and interp_atomic ist tac : unit Proofview.tactic = (name_atomic ~env (TacInversion (NonDepInversion (k,hyps,ids),dqhyps)) (Inv.inv_clause k ids_interp hyps dqhyps)) sigma - end + end } | TacInversion (InversionUsing (c,idl),hyp) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let (sigma,c_interp) = interp_constr ist env sigma c in @@ -2259,7 +2259,7 @@ and interp_atomic ist tac : unit Proofview.tactic = name_atomic ~env (TacInversion (InversionUsing (c_interp,hyps),dqhyps)) (Leminv.lemInv_clause dqhyps c_interp hyps) - end + end } (* Initial call for interpretation *) @@ -2280,7 +2280,7 @@ let eval_tactic_ist ist t = let interp_tac_gen lfun avoid_ids debug t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let extra = TacStore.set TacStore.empty f_debug debug in let extra = TacStore.set extra f_avoid_ids avoid_ids in @@ -2289,7 +2289,7 @@ let interp_tac_gen lfun avoid_ids debug t = interp_tactic ist (intern_pure_tactic { ltacvars; genv = env } t) - end + end } let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t let _ = Proof_global.set_interp_tac interp @@ -2309,9 +2309,9 @@ let hide_interp global t ot = Proofview.tclENV >>= fun env -> hide_interp env else - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> hide_interp (Proofview.Goal.env gl) - end + end } (***************************************************************************) (** Register standard arguments *) @@ -2411,7 +2411,7 @@ let _ = Hook.set Auto.extern_interp let dummy_id = Id.of_string "_" let lift_constr_tac_to_ml_tac vars tac = - let tac _ ist = Proofview.Goal.enter begin fun gl -> + let tac _ ist = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let map = function @@ -2424,5 +2424,5 @@ let lift_constr_tac_to_ml_tac vars tac = in let args = List.map_filter map vars in tac args ist - end in + end } in tac diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index bc82e9ef4..3c56bbdc0 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -538,66 +538,65 @@ module New = struct mkVar (nthHypId m gl) let onNthHypId m tac = - Proofview.Goal.enter begin fun gl -> tac (nthHypId m gl) end + Proofview.Goal.enter { enter = begin fun gl -> tac (nthHypId m gl) end } let onNthHyp m tac = - Proofview.Goal.enter begin fun gl -> tac (nthHyp m gl) end + Proofview.Goal.enter { enter = begin fun gl -> tac (nthHyp m gl) end } let onLastHypId = onNthHypId 1 let onLastHyp = onNthHyp 1 let onNthDecl m tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> Proofview.tclUNIT (nthDecl m gl) >>= tac - end + end } let onLastDecl = onNthDecl 1 let ifOnHyp pred tac1 tac2 id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let typ = Tacmach.New.pf_get_hyp_typ id gl in if pred (id,typ) then tac1 id else tac2 id - end + end } - let onHyps find tac = Proofview.Goal.nf_enter (fun gl -> tac (find gl)) + let onHyps find tac = Proofview.Goal.nf_enter { enter = begin fun gl -> tac (find gl) end } let afterHyp id tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let hyps = Proofview.Goal.hyps gl in let rem, _ = List.split_when (fun (hyp,_,_) -> Id.equal hyp id) hyps in tac rem - end + end } let fullGoal gl = let hyps = Tacmach.New.pf_ids_of_hyps gl in None :: List.map Option.make hyps let tryAllHyps tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let hyps = Tacmach.New.pf_ids_of_hyps gl in tclFIRST_PROGRESS_ON tac hyps - end + end } let tryAllHypsAndConcl tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> tclFIRST_PROGRESS_ON tac (fullGoal gl) - end + end } let onClause tac cl = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let hyps = Tacmach.New.pf_ids_of_hyps gl in tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl) - end + end } (* Find the right elimination suffix corresponding to the sort of the goal *) (* c should be of type A1->.. An->B with B an inductive definition *) let general_elim_then_using mk_elim isrec allnames tac predicate ind (c, t) = - Proofview.Goal.nf_enter - begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (Proofview.Goal.nf_enter begin fun gl -> + (Proofview.Goal.nf_enter { enter = begin fun gl -> let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in (* applying elimination_scheme just a little modified *) let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in @@ -649,10 +648,10 @@ module New = struct Proofview.tclTHEN (Clenvtac.clenv_refine false clenv') (Proofview.tclEXTEND [] tclIDTAC branchtacs) - end) end + end }) end } let elimination_then tac c = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with @@ -660,7 +659,7 @@ module New = struct | Some _ -> false,gl_make_case_dep in general_elim_then_using mkelim isrec None tac None ind (c, t) - end + end } let case_then_using = general_elim_then_using gl_make_case_dep false @@ -669,16 +668,16 @@ module New = struct general_elim_then_using gl_make_case_nodep false let elim_on_ba tac ba = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let branches = Tacmach.New.of_old (make_elim_branch_assumptions ba) gl in tac branches - end + end } let case_on_ba tac ba = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let branches = Tacmach.New.of_old (make_case_branch_assumptions ba) gl in tac branches - end + end } let elimination_sort_of_goal gl = (** Retyping will expand evars anyway. *) @@ -695,11 +694,11 @@ module New = struct | Some id -> elimination_sort_of_hyp id gl let pf_constr_of_global ref tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> 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.Unsafe.tclEVARS sigma <*> (tac c) - end + end } end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d3cf154c9..66053a314 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -184,7 +184,7 @@ let unsafe_intro env store (id, c, t) b = end } let introduction ?(check=true) id = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let sigma = Proofview.Goal.sigma gl in @@ -199,12 +199,12 @@ let introduction ?(check=true) id = | Prod (_, t, b) -> unsafe_intro env store (id, None, t) b | LetIn (_, c, t, b) -> unsafe_intro env store (id, Some c, t) b | _ -> raise (RefinerError IntroNeedsProduct) - end + end } let refine = Tacmach.refine let convert_concl ?(check=true) ty k = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in let conclty = Proofview.Goal.raw_concl gl in @@ -221,10 +221,10 @@ let convert_concl ?(check=true) ty k = let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in Sigma (ans, sigma, p +> q) end } - end + end } let convert_hyp ?(check=true) d = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let ty = Proofview.Goal.raw_concl gl in @@ -234,20 +234,20 @@ let convert_hyp ?(check=true) d = Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> Evarutil.new_evar env sigma ~principal:true ~store ty end } - end + end } let convert_concl_no_check = convert_concl ~check:false let convert_hyp_no_check = convert_hyp ~check:false let convert_gen pb x y = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> try let sigma = Tacmach.New.pf_apply Evd.conversion gl pb x y in Proofview.Unsafe.tclEVARS sigma with (* Reduction.NotConvertible *) _ -> (** FIXME: Sometimes an anomaly is raised from conversion *) Tacticals.New.tclFAIL 0 (str "Not convertible") -end +end } let convert x y = convert_gen Reduction.CONV x y let convert_leq x y = convert_gen Reduction.CUMUL x y @@ -319,7 +319,7 @@ let rename_hyp repl = match dom with | None -> Tacticals.New.tclZEROMSG (str "Not a one-to-one name mapping") | Some (src, dst) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in let concl = Proofview.Goal.concl gl in @@ -356,7 +356,7 @@ let rename_hyp repl = let (sigma, c) = Evarutil.new_evar_instance nctx sigma nconcl ~store instance in Sigma.Unsafe.of_pair (c, sigma) end } - end + end } (**************************************************************) (* Fresh names *) @@ -417,7 +417,7 @@ let find_name mayrepl decl naming gl = match naming with (**************************************************************) let assert_before_then_gen b naming t tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let id = find_name b (Anonymous,None,t) naming gl in Tacticals.New.tclTHENLAST (Proofview.V82.tactic @@ -426,7 +426,7 @@ let assert_before_then_gen b naming t tac = with Evarutil.ClearDependencyError (id,err) -> error_replacing_dependency (pf_env gl) (project gl) id err)) (tac id) - end + end } let assert_before_gen b naming t = assert_before_then_gen b naming t (fun _ -> Proofview.tclUNIT ()) @@ -435,7 +435,7 @@ let assert_before na = assert_before_gen false (naming_of_name na) let assert_before_replacing id = assert_before_gen true (NamingMustBe (dloc,id)) let assert_after_then_gen b naming t tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let id = find_name b (Anonymous,None,t) naming gl in Tacticals.New.tclTHENFIRST (Proofview.V82.tactic @@ -444,7 +444,7 @@ let assert_after_then_gen b naming t tac = with Evarutil.ClearDependencyError (id,err) -> error_replacing_dependency (pf_env gl) (project gl) id err)) (tac id) - end + end } let assert_after_gen b naming t = assert_after_then_gen b naming t (fun _ -> (Proofview.tclUNIT ())) @@ -783,7 +783,7 @@ let build_intro_tac id dest tac = match dest with Proofview.V82.tactic (move_hyp id dest); tac id] let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in let concl = nf_evar (Proofview.Goal.sigma gl) concl in match kind_of_term concl with @@ -809,7 +809,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = Tacticals.New.tclZEROMSG (str "No product even after head-reduction.") | e -> Proofview.tclZERO ~info e end - end + end } let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ()) let intro_mustbe_force id = intro_gen (NamingMustBe (dloc,id)) MoveLast true false @@ -873,14 +873,14 @@ let get_previous_hyp_position id gl = aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) let intro_replacing id = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let next_hyp = get_next_hyp_position id gl in Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (thin_for_replacing [id]); introduction id; Proofview.V82.tactic (move_hyp id next_hyp); ] - end + end } (* We have e.g. [x, y, y', x', y'' |- forall y y' y'', G] and want to reintroduce y, y,' y''. Note that we have to clear y, y' and y'' @@ -892,7 +892,7 @@ let intro_replacing id = (* the behavior of inversion *) let intros_possibly_replacing ids = let suboptimal = true in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in Tacticals.New.tclTHEN (Tacticals.New.tclMAP (fun id -> @@ -901,16 +901,16 @@ let intros_possibly_replacing ids = (Tacticals.New.tclMAP (fun (id,pos) -> Tacticals.New.tclORELSE (intro_move (Some id) pos) (intro_using id)) posl) - end + end } (* This version assumes that replacement is actually possible *) let intros_replacing ids = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in Tacticals.New.tclTHEN (Proofview.V82.tactic (thin_for_replacing ids)) (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl) - end + end } (* User-level introduction tactics *) @@ -954,10 +954,10 @@ let depth_of_quantified_hypothesis red h gl = str".") let intros_until_gen red h = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let n = Tacmach.New.of_old (depth_of_quantified_hypothesis red h) gl in Tacticals.New.tclDO n (if red then introf else intro) - end + end } let intros_until_id id = intros_until_gen false (NamedHyp id) let intros_until_n_gen red n = intros_until_gen red (AnonHyp n) @@ -998,20 +998,20 @@ let onOpenInductionArg env sigma tac = function (intros_until_n n) (Tacticals.New.onLastHyp (fun c -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let pending = (sigma,sigma) in tac clear_flag (pending,(c,NoBindings)) - end)) + end })) | clear_flag,ElimOnIdent (_,id) -> (* A quantified hypothesis *) Tacticals.New.tclTHEN (try_intros_until_id_check id) - (Proofview.Goal.enter begin fun gl -> + (Proofview.Goal.enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let pending = (sigma,sigma) in tac clear_flag (pending,(mkVar id,NoBindings)) - end) + end }) let onInductionArg tac = function | clear_flag,ElimOnConstr cbl -> @@ -1036,7 +1036,7 @@ let map_induction_arg f = function (****************************************) let cut c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let concl = Tacmach.New.pf_nf_concl gl in @@ -1062,7 +1062,7 @@ let cut c = end } else Tacticals.New.tclZEROMSG (str "Not a proposition or a type.") - end + end } let error_uninstantiated_metas t clenv = let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in @@ -1171,12 +1171,12 @@ let enforce_prop_bound_names rename tac = mkLetIn (na,c,t,aux (push_rel (na,Some c,t) env) sigma (i-1) t') | _ -> print_int i; Pp.msg (print_constr t); assert false in let rename_branch i = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let t = Proofview.Goal.concl gl in change_concl (aux env sigma i t) - end in + end } in (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) tac (Array.map rename_branch nn) @@ -1191,7 +1191,7 @@ let rec contract_letin_in_lam_header c = let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ()) rename i (elim, elimty, bindings) indclause = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let elim = contract_letin_in_lam_header elim in @@ -1204,7 +1204,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags in let elimclause' = clenv_fchain ~flags indmv elimclause indclause in enforce_prop_bound_names rename (Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags) - end + end } (* * Elimination tactic with bindings and using an arbitrary @@ -1221,7 +1221,7 @@ type eliminator = { } let general_elim_clause_gen elimtac indclause elim = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let (elimc,lbindelimc) = elim.elimbody in @@ -1229,10 +1229,10 @@ let general_elim_clause_gen elimtac indclause elim = let i = match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause - end + end } let general_elim with_evars clear_flag (c, lbindc) elim = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let ct = Retyping.get_type_of env sigma c in @@ -1242,7 +1242,7 @@ let general_elim with_evars clear_flag (c, lbindc) elim = Tacticals.New.tclTHEN (general_elim_clause_gen elimtac indclause elim) (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c) - end + end } (* Case analysis tactics *) @@ -1349,7 +1349,7 @@ let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause = let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (elim, elimty, bindings) indclause = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let elim = contract_letin_in_lam_header elim in @@ -1372,7 +1372,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) (str "Nothing to rewrite in " ++ pr_id id ++ str"."); clenv_refine_in with_evars id id sigma elimclause'' (fun id -> Proofview.tclUNIT ()) - end + end } let general_elim_clause with_evars flags id c e = let elim = match id with @@ -1427,7 +1427,7 @@ let make_projection env sigma params cstr sign elim i n c u = in elim let descend_in_conjunctions avoid tac (err, info) c = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in try @@ -1448,7 +1448,7 @@ let descend_in_conjunctions avoid tac (err, info) c = NotADefinedRecordUseScheme (snd elim) in Tacticals.New.tclFIRST (List.init n (fun i -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in match make_projection env sigma params cstr sign elim i n c u with @@ -1459,10 +1459,10 @@ let descend_in_conjunctions avoid tac (err, info) c = [Proofview.V82.tactic (refine p); (* Might be ill-typed due to forbidden elimination. *) Tacticals.New.onLastHypId (tac (not isrec))] - end)) + end })) | None -> Proofview.tclZERO ~info err with RefinerError _|UserError _ -> Proofview.tclZERO ~info err - end + end } (****************************************************) (* Resolution tactics *) @@ -1495,7 +1495,7 @@ let tclORELSEOPT t k = | Some tac -> tac) let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let flags = if with_delta then default_unify_flags () else default_no_delta_unify_flags () in @@ -1504,7 +1504,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) step. *) let concl_nprod = nb_prod concl in let rec try_main_apply with_destruct c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in @@ -1558,14 +1558,14 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) | PretypeError _|RefinerError _|UserError _|Failure _ -> Some (try_red_apply thm_ty0 (e, info)) | _ -> None) - end + end } in Tacticals.New.tclTHENLIST [ try_main_apply with_destruct c; solve_remaining_apply_goals; apply_clear_request clear_flag (use_clear_hyp_by_default ()) c ] - end + end } let rec apply_with_bindings_gen b e = function | [] -> Proofview.tclUNIT () @@ -1577,13 +1577,13 @@ let rec apply_with_bindings_gen b e = function let apply_with_delayed_bindings_gen b e l = let one k (loc, f) = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let (cb, sigma) = run_delayed env sigma f in Tacticals.New.tclWITHHOLES e (general_apply b b e k (loc,cb)) sigma - end + end } in let rec aux = function | [] -> Proofview.tclUNIT () @@ -1646,7 +1646,7 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) = let apply_in_once sidecond_first with_delta with_destruct with_evars naming id (clear_flag,(loc,(d,lbind))) tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let flags = @@ -1655,7 +1655,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in let targetid = find_name true (Anonymous,None,t') naming gl in let rec aux idstoclear with_destruct c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in try @@ -1672,14 +1672,14 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming (descend_in_conjunctions [targetid] (fun b id -> aux (id::idstoclear) b (mkVar id)) (e, info) c) - end + end } in aux [] with_destruct d - end + end } let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming id (clear_flag,(loc,f)) tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let (c, sigma) = run_delayed env sigma f in @@ -1687,7 +1687,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam (apply_in_once sidecond_first with_delta with_destruct with_evars naming id (clear_flag,(loc,c)) tac) sigma - end + end } (* A useful resolution tactic which, if c:A->B, transforms |- C into |- B -> C and |- A @@ -1707,7 +1707,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam *) let cut_and_apply c = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) -> let concl = Proofview.Goal.concl gl in @@ -1720,7 +1720,7 @@ let cut_and_apply c = Sigma (ans, sigma, p +> q) end } | _ -> error "lapply needs a non-dependent product." - end + end } (********************************************************************) (* Exact tactics *) @@ -1780,10 +1780,10 @@ let assumption = Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar id) h } else arec gl only_eq rest in - let assumption_tac gl = + let assumption_tac = { enter = begin fun gl -> let hyps = Proofview.Goal.hyps gl in arec gl true hyps - in + end } in Proofview.Goal.nf_enter assumption_tac (*****************************************************************) @@ -1826,7 +1826,7 @@ let check_decl env (_, c, ty) msg = msg e let clear_body ids = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in let ctx = named_context env in @@ -1862,7 +1862,7 @@ let clear_body ids = Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> Evarutil.new_evar env sigma concl end } - end + end } let clear_wildcards ids = Proofview.V82.tactic (tclMAP (fun (loc,id) gl -> @@ -1922,7 +1922,7 @@ let specialize (c,lbind) g = (* Keeping only a few hypotheses *) let keep hyps = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> Proofview.tclENV >>= fun env -> let ccl = Proofview.Goal.concl gl in let cl,_ = @@ -1935,7 +1935,7 @@ let keep hyps = ~init:([],[]) (Proofview.Goal.env gl) in Proofview.V82.tactic (fun gl -> thin cl gl) - end + end } (************************) (* Introduction tactics *) @@ -1991,7 +1991,7 @@ let rec tclANY tac = function let any_constructor with_evars tacopt = let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in let tac i = Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let cl = Tacmach.New.pf_nf_concl gl in let reduce_to_quantified_ind = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl @@ -2001,7 +2001,7 @@ let any_constructor with_evars tacopt = Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in if Int.equal nconstr 0 then error "The type has no constructors."; tclANY tac (List.interval 1 nconstr) - end + end } let left_with_bindings with_evars = constructor_tac with_evars (Some 2) 1 let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2 @@ -2052,7 +2052,7 @@ let my_find_eq_data_decompose gl t = | Constr_matching.PatternMatchingFailure -> None let intro_decomp_eq loc l thin tac id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in @@ -2063,10 +2063,10 @@ let intro_decomp_eq loc l thin tac id = (eq,t,eq_args) (c, t) | None -> Tacticals.New.tclZEROMSG (str "Not a primitive equality here.") - end + end } let intro_or_and_pattern loc bracketed ll thin tac id = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in @@ -2077,7 +2077,7 @@ let intro_or_and_pattern loc bracketed ll thin tac id = (Tacticals.New.tclTHEN (simplest_case c) (Proofview.V82.tactic (clear [id]))) (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l) nv (Array.of_list ll)) - end + end } let rewrite_hyp assert_style l2r id = let rew_on l2r = @@ -2085,7 +2085,7 @@ let rewrite_hyp assert_style l2r id = let subst_on l2r x rhs = Hook.get forward_subst_one true x (id,rhs,l2r) in let clear_var_and_eq c = tclTHEN (clear [id]) (clear [destVar c]) in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in @@ -2107,7 +2107,7 @@ let rewrite_hyp assert_style l2r id = Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id])) | _ -> Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id])) - end + end } let rec prepare_naming loc = function | IntroIdentifier id -> NamingMustBe (loc,id) @@ -2243,7 +2243,7 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with Proofview.tclUNIT () (* apply_in_once do a replacement *) else Proofview.V82.tactic (clear [id]) in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let (c, sigma) = run_delayed env sigma f in @@ -2255,7 +2255,7 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with (fun id -> Tacticals.New.tclTHEN doclear (tac_ipat id))) (tac thin None [])) sigma - end + end } and prepare_intros_loc loc dft destopt = function | IntroNaming ipat -> @@ -2318,7 +2318,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars let tac (naming,lemma) tac id = apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming id lemma tac in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let destopt = if with_evars then MoveLast (* evars would depend on the whole context *) else get_previous_hyp_position id gl in @@ -2329,7 +2329,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars in (* We chain apply_in_once, ending with an intro pattern *) List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id - end + end } (* if sidecond_first then @@ -2477,12 +2477,12 @@ let letin_pat_tac with_eq id c occs = let forward b usetac ipat c = match usetac with | None -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let t = Tacmach.New.pf_unsafe_type_of gl c in let hd = head_ident c in Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (Proofview.V82.tactic (exact_no_check c)) - end + end } | Some tac -> if b then Tacticals.New.tclTHENFIRST (assert_as b None ipat c) tac @@ -2512,7 +2512,7 @@ let apply_type hdcty argl gl = let bring_hyps hyps = if List.is_empty hyps then Tacticals.New.tclIDTAC else - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let concl = Tacmach.New.pf_nf_concl gl in let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in @@ -2521,14 +2521,14 @@ let bring_hyps hyps = let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma newcl in Sigma (mkApp (ev, args), sigma, p) end } - end + end } let revert hyps = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in (bring_hyps ctx) <*> (Proofview.V82.tactic (clear hyps)) - end + end } (* Compute a name for a generalization *) @@ -2809,7 +2809,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names = match ra with | (RecArg,deprec,recvarname) :: (IndArg,depind,hyprecname) :: ra' -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (recpat,names) = match names with | [loc,IntroNaming (IntroIdentifier id) as pat] -> let id' = next_ident_away (add_prefix "IH" id) avoid in @@ -2817,37 +2817,37 @@ let induct_discharge dests avoid' tac (avoid,ra) names = | _ -> consume_pattern avoid (Name recvarname) deprec gl names in let dest = get_recarg_dest dests in dest_intro_patterns avoid thin dest [recpat] (fun ids thin -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (hyprec,names) = consume_pattern avoid (Name hyprecname) depind gl names in dest_intro_patterns avoid thin MoveLast [hyprec] (fun ids' thin -> peel_tac ra' (update_dest dests ids') names thin) - end) - end + end }) + end } | (IndArg,dep,hyprecname) :: ra' -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> (* Rem: does not happen in Coq schemes, only in user-defined schemes *) let pat,names = consume_pattern avoid (Name hyprecname) dep gl names in dest_intro_patterns avoid thin MoveLast [pat] (fun ids thin -> peel_tac ra' (update_dest dests ids) names thin) - end + end } | (RecArg,dep,recvarname) :: ra' -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (pat,names) = consume_pattern avoid (Name recvarname) dep gl names in let dest = get_recarg_dest dests in dest_intro_patterns avoid thin dest [pat] (fun ids thin -> peel_tac ra' dests names thin) - end + end } | (OtherArg,dep,_) :: ra' -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (pat,names) = consume_pattern avoid Anonymous dep gl names in let dest = get_recarg_dest dests in safe_dest_intro_patterns avoid thin dest [pat] (fun ids thin -> peel_tac ra' dests names thin) - end + end } | [] -> check_unused_names names; Tacticals.New.tclTHEN (clear_wildcards thin) (tac dests) @@ -2861,7 +2861,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names = (* Marche pas... faut prendre en compte l'occurrence précise... *) let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 (Proofview.Goal.assume gl) in let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in @@ -2910,7 +2910,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = (atomize_one (i-1) (mkVar x::args) (x::avoid)) in atomize_one (List.length argl) [] [] - end + end } (* [cook_sign] builds the lists [beforetoclear] (preceding the ind. var.) and [aftertoclear] (coming after the ind. var.) of hyps @@ -3362,7 +3362,7 @@ let abstract_args gl generalize_vars dep id defined f args = else None let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> Coqlib.check_required_library Coqlib.jmeq_module_name; let (f, args, def, id, oldid) = let oldid = Tacmach.New.pf_get_new_id id gl in @@ -3394,7 +3394,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = [revert vars ; Proofview.V82.tactic (fun gl -> tclMAP (fun id -> tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)]) - end + end } let rec compare_upto_variables x y = if (isVar x || isRel x) && (isVar y || isRel y) then true @@ -3817,12 +3817,12 @@ let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac = end } let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let elim_info = find_induction_type isrec elim hyp0 (Proofview.Goal.assume gl) in atomize_param_of_ind_then elim_info hyp0 (fun indvars -> apply_induction_in_context (Some hyp0) inhyps (pi3 elim_info) indvars names (fun elim -> Proofview.V82.tactic (induction_tac with_evars [] [hyp0] elim))) - end + end } let msg_not_right_number_induction_arguments scheme = str"Not the right number of induction arguments (expected " ++ @@ -3839,7 +3839,7 @@ let msg_not_right_number_induction_arguments scheme = must be given, so we help a bit the unifier by making the "pattern" by hand before calling induction_tac *) let induction_without_atomization isrec with_evars elim names lid = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let sigma, (indsign,scheme) = get_elim_signature elim (List.hd lid) gl in let nargs_indarg_farg = scheme.nargs + (if scheme.farg_in_concl then 1 else 0) in @@ -3870,7 +3870,7 @@ let induction_without_atomization isrec with_evars elim names lid = ]) in let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in apply_induction_in_context None [] elim indvars names induct_tac - end + end } (* assume that no occurrences are selected *) let clear_unselected_context id inhyps cls gl = @@ -4021,7 +4021,7 @@ let induction_gen clear_flag isrec with_evars elim let inhyps = match cls with | Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps | _ -> [] in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let ccl = Proofview.Goal.raw_concl gl in @@ -4057,7 +4057,7 @@ let induction_gen clear_flag isrec with_evars elim isrec with_evars info_arg elim id arg t inhyps cls (induction_with_atomization_of_ind_arg isrec with_evars elim names id inhyps) - end + end } (* Induction on a list of arguments. First make induction arguments atomic (using letins), then do induction. The specificity here is @@ -4082,7 +4082,7 @@ let induction_gen_l isrec with_evars elim names lc = atomize_list l' | _ -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in let x = id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in @@ -4093,7 +4093,7 @@ let induction_gen_l isrec with_evars elim names lc = Tacticals.New.tclTHEN (letin_tac None (Name id) c None allHypsAndConcl) (atomize_list newl') - end in + end } in Tacticals.New.tclTHENLIST [ (atomize_list lc); @@ -4110,7 +4110,7 @@ let induction_destruct isrec with_evars (lc,elim) = match lc with | [] -> assert false (* ensured by syntax, but if called inside caml? *) | [c,(eqname,names as allnames),cls] -> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in match elim with @@ -4135,9 +4135,9 @@ let induction_destruct isrec with_evars (lc,elim) = (* standard induction *) onOpenInductionArg env sigma (fun clear_flag c -> induction_gen clear_flag isrec with_evars elim (c,allnames) cls) c - end + end } | _ -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in match elim with @@ -4153,12 +4153,12 @@ let induction_destruct isrec with_evars (lc,elim) = (onOpenInductionArg env sigma (fun clear_flag a -> induction_gen clear_flag isrec with_evars None (a,b) cl) a) (Tacticals.New.tclMAP (fun (a,b,cl) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in onOpenInductionArg env sigma (fun clear_flag a -> induction_gen clear_flag false with_evars None (a,b) cl) a - end) l) + end }) l) | Some elim -> (* Several induction hyps with induction scheme *) let finish_evar_resolution f = @@ -4186,7 +4186,7 @@ let induction_destruct isrec with_evars (lc,elim) = error "'as' clause with multiple arguments and 'using' clause can only occur last."; let newlc = List.map (fun (x,_) -> (x,None)) newlc in induction_gen_l isrec with_evars elim names newlc - end + end } let induction ev clr c l e = induction_gen clr true ev e @@ -4228,7 +4228,7 @@ let simple_destruct = function *) let elim_scheme_type elim t = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let clause = Tacmach.New.of_old (fun gl -> mk_clenv_type_of gl elim) gl in match kind_of_term (last_arg clause.templval.rebus) with | Meta mv -> @@ -4238,7 +4238,7 @@ let elim_scheme_type elim t = (clenv_meta_type clause mv) clause in Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false | _ -> anomaly (Pp.str "elim_scheme_type") - end + end } let elim_type t = Proofview.Goal.s_enter { s_enter = begin fun gl sigma -> @@ -4274,7 +4274,7 @@ let maybe_betadeltaiota_concl allowred gl = whd_betadeltaiota env sigma concl let reflexivity_red allowred = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> (* PL: usual reflexivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) @@ -4282,7 +4282,7 @@ let reflexivity_red allowred = match match_with_equality_type concl with | None -> Proofview.tclZERO NoEquationFound | Some _ -> one_constructor 1 NoBindings - end + end } let reflexivity = Proofview.tclORELSE @@ -4324,7 +4324,7 @@ let match_with_equation c = Proofview.tclZERO NoEquationFound let symmetry_red allowred = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> (* PL: usual symmetry don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) @@ -4336,7 +4336,7 @@ let symmetry_red allowred = (convert_concl_no_check concl DEFAULTcast) (Tacticals.New.pf_constr_of_global eq_data.sym apply) | None,eq,eq_kind -> prove_symmetry eq eq_kind - end + end } let symmetry = Proofview.tclORELSE @@ -4350,7 +4350,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make () let symmetry_in id = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in let sign,t = decompose_prod_assum ctype in Proofview.tclORELSE @@ -4368,7 +4368,7 @@ let symmetry_in id = | NoEquationFound -> Hook.get forward_setoid_symmetry_in id | e -> Proofview.tclZERO ~info e end - end + end } let intros_symmetry = Tacticals.New.onClause @@ -4393,7 +4393,7 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make () (* This is probably not very useful any longer *) let prove_transitivity hdcncl eq_kind t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (eq1,eq2) = match eq_kind with | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]) @@ -4413,10 +4413,10 @@ let prove_transitivity hdcncl eq_kind t = [ Tacticals.New.tclDO 2 intro; Tacticals.New.onLastHyp simplest_case; assumption ])) - end + end } let transitivity_red allowred t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> (* PL: usual transitivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) @@ -4433,7 +4433,7 @@ let transitivity_red allowred t = match t with | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.") | Some t -> prove_transitivity eq eq_kind t - end + end } let transitivity_gen t = Proofview.tclORELSE diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 59c579237..9bee7ab3e 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -18,6 +18,7 @@ open Tacinterp open Tactics open Errors open Util +open Proofview.Notations DECLARE PLUGIN "tauto" @@ -305,13 +306,13 @@ let reduction_not_iff _ist = let t_reduction_not_iff = tacticIn reduction_not_iff let intuition_gen ist flags tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let tac = Value.of_closure ist tac in let env = Proofview.Goal.env gl in let vars, ist, intuition = tauto_intuit flags t_reduction_not_iff tac in let glb_intuition = Tacintern.glob_tactic_env vars env intuition in eval_tactic_ist ist glb_intuition - end + end } let tauto_intuitionistic flags = Proofview.tclORELSE diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 8ac273c84..8282ce30b 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -355,7 +355,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = ))) ) in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in let u,v = destruct_ind type_of_pq in let lb_type_of_p = @@ -385,7 +385,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = Tacticals.New.tclTHENLIST [ Proofview.tclEFFECTS eff; Equality.replace p q ; apply app ; Auto.default_auto] - end + end } (* used in the bool -> leib side *) let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = @@ -417,7 +417,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let rec aux l1 l2 = match (l1,l2) with | (t1::q1,t2::q2) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in if eq_constr t1 t2 then aux q1 q2 else ( @@ -458,7 +458,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = aux q1 q2 ] ) ) - end + end } | ([],[]) -> Proofview.tclUNIT () | _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.") in @@ -565,7 +565,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = avoid := fresh::(!avoid); fresh end gl in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in let freshn = fresh_id (Id.of_string "x") gl in let freshm = fresh_id (Id.of_string "y") gl in @@ -588,18 +588,18 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). Tacticals.New.tclREPEAT ( Tacticals.New.tclTHENLIST [ Simple.apply_in freshz (andb_prop()); - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let fresht = fresh_id (Id.of_string "Z") gl in (destruct_on_as (mkVar freshz) [[dl,IntroNaming (IntroIdentifier fresht); dl,IntroNaming (IntroIdentifier freshz)]]) - end + end } ]); (* Ci a1 ... an = Ci b1 ... bn replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto *) - Proofview.Goal.nf_enter begin fun gls -> + Proofview.Goal.nf_enter { enter = begin fun gls -> let gl = Proofview.Goal.concl gls in match (kind_of_term gl) with | App (c,ca) -> ( @@ -618,10 +618,10 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.") ) | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") - end + end } ] - end + end } let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined") @@ -708,7 +708,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = avoid := fresh::(!avoid); fresh end gl in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in let freshn = fresh_id (Id.of_string "x") gl in let freshm = fresh_id (Id.of_string "y") gl in @@ -731,7 +731,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = Tacticals.New.tclTHENLIST [apply (andb_true_intro()); simplest_split ;Auto.default_auto ] ); - Proofview.Goal.nf_enter begin fun gls -> + Proofview.Goal.nf_enter { enter = begin fun gls -> let gl = Proofview.Goal.concl gls in (* assume the goal to be eq (eq_type ...) = true *) match (kind_of_term gl) with @@ -747,9 +747,9 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = ) | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") - end + end } ] - end + end } let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined") @@ -855,7 +855,7 @@ let compute_dec_tact ind lnamesparrec nparrec = avoid := fresh::(!avoid); fresh end gl in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in let freshn = fresh_id (Id.of_string "x") gl in let freshm = fresh_id (Id.of_string "y") gl in @@ -886,7 +886,7 @@ let compute_dec_tact ind lnamesparrec nparrec = ) (Tacticals.New.tclTHEN (destruct_on eqbnm) Auto.default_auto); - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let freshH2 = fresh_id (Id.of_string "H") gl in Tacticals.New.tclTHENS (destruct_on_using (mkVar freshH) freshH2) [ (* left *) @@ -898,7 +898,7 @@ let compute_dec_tact ind lnamesparrec nparrec = ; (*right *) - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let freshH3 = fresh_id (Id.of_string "H") gl in Tacticals.New.tclTHENLIST [ simplest_right ; @@ -920,11 +920,11 @@ let compute_dec_tact ind lnamesparrec nparrec = true; Equality.discr_tac false None ] - end + end } ] - end + end } ] - end + end } let make_eq_decidability mode mind = let mib = Global.lookup_mind mind in |