diff options
Diffstat (limited to 'plugins')
30 files changed, 379 insertions, 455 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 33a9dd4fd..6281b2675 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -1,5 +1,3 @@ -open Proofview.Notations - let contrib_name = "btauto" let init_constant dir s = @@ -219,7 +217,7 @@ module Btauto = struct Tacticals.tclFAIL 0 msg gl let try_unification env = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in let eq = Lazy.force eq in let concl = EConstr.Unsafe.to_constr concl in @@ -232,10 +230,10 @@ module Btauto = struct | _ -> let msg = str "Btauto: Internal error" in Tacticals.New.tclFAIL 0 msg - end } + end let tac = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in let concl = EConstr.Unsafe.to_constr concl in let sigma = Tacmach.New.project gl in @@ -262,6 +260,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 43c06a54d..b638f2360 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -241,24 +241,20 @@ let app_global f args k = Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> k (mkApp (fc, args)) let rec gen_holes env sigma t n accu = - let open Sigma in if Int.equal n 0 then (sigma, List.rev accu) else match EConstr.kind sigma t with | Prod (_, u, t) -> - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (ev, sigma, _) = Evarutil.new_evar env sigma u in - let sigma = Sigma.to_evar_map sigma in + let (sigma, ev) = Evarutil.new_evar env sigma u in let t = EConstr.Vars.subst1 ev t in gen_holes env sigma t (pred n) (ev :: accu) | _ -> assert false let app_global_with_holes f args n = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - Refine.refine { Sigma.run = begin fun sigma -> - let sigma = Sigma.to_evar_map sigma in + Refine.refine begin fun sigma -> let t = Tacmach.New.pf_get_type_of gl fc in let t = Termops.prod_applist sigma t (Array.to_list args) in let ans = mkApp (fc, args) in @@ -266,32 +262,33 @@ let app_global_with_holes f args n = let ans = applist (ans, holes) in let evdref = ref sigma in let () = Typing.e_check env evdref ans concl in - Sigma.Unsafe.of_pair (ans, !evdref) - end } - end } + (!evdref, ans) + end + end let assert_before n c = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let evm, _ = Tacmach.New.pf_apply type_of gl c in - Sigma.Unsafe.of_pair (assert_before n c, evm) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) + (assert_before n c) + end let refresh_type env evm ty = Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true (Some false) env evm ty let refresh_universes ty k = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let evm = Tacmach.New.project gl in let evm, ty = refresh_type env evm ty in - Sigma.Unsafe.of_pair (k ty, evm) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k ty) + end let constr_of_term c = EConstr.of_constr (constr_of_term c) let rec proof_tac p : unit Proofview.tactic = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.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 @@ -354,10 +351,10 @@ let rec proof_tac p : unit Proofview.tactic = Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Tacticals.New.tclTHEN injt (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.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in let false_t=mkApp (c,[|mkVar hid|]) in @@ -366,16 +363,16 @@ let refute_tac c t1 t2 p = Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; simplest_elim false_t] in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k - end } + end let refine_exact_check c = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let evm, _ = Tacmach.New.pf_apply type_of gl c in - Sigma.Unsafe.of_pair (exact_check c, evm) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (exact_check c) + end let convert_to_goal_tac c t1 t2 p = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let k sort = let neweq= app_global _eq [|sort;tt1;tt2|] in @@ -386,21 +383,21 @@ let convert_to_goal_tac c t1 t2 p = Tacticals.New.tclTHENS (neweq (assert_before (Name e))) [proof_tac p; endt refine_exact_check] in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k - end } + end let convert_to_hyp_tac c1 t1 c2 t2 p = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let tt2=constr_of_term t2 in let h = Tacmach.New.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 (* Essentially [assert (Heq : lhs = rhs) by proof_tac p; discriminate Heq] *) let discriminate_tac cstru p = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let lhs=constr_of_term p.p_lhs and rhs=constr_of_term p.p_rhs in let env = Proofview.Goal.env gl in let evm = Tacmach.New.project gl in @@ -410,7 +407,7 @@ let discriminate_tac cstru p = Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) (Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; Equality.discrHyp hid]) - end } + end (* wrap everything *) @@ -421,7 +418,7 @@ let build_term_to_complete uf pac = (applist (mkConstructU (kn, EInstance.make u), real_args), pac.arity) let cc_tactic depth additionnal_terms = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in Coqlib.check_required_library Coqlib.logic_module_name; let _ = debug (fun () -> Pp.str "Reading subgoal ...") in @@ -477,7 +474,7 @@ let cc_tactic depth additionnal_terms = let ida = EConstr.of_constr ida in let idb = EConstr.of_constr idb in convert_to_hyp_tac ida ta idb tb p - end } + end let cc_fail = Tacticals.New.tclZEROMSG (Pp.str "congruence failed.") @@ -500,17 +497,17 @@ 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.s_enter { s_enter = begin fun gl -> + Proofview.Goal.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 let term = mkApp (fc, [| ty; c1; c2 |]) in let evm, _ = type_of (pf_env gl) evm term in - Sigma.Unsafe.of_pair (k term, evm) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k term) + end let f_equal = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let cut_eq c1 c2 = @@ -537,4 +534,4 @@ let f_equal = | Pretype_errors.PretypeError _ | Type_errors.TypeError _ -> Proofview.tclUNIT () | e -> Proofview.tclZERO ~info e end - end } + end diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index bbb9feae2..e3fab6d01 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -15,7 +15,6 @@ open Ground open Goptions open Tacmach.New open Tacticals.New -open Proofview.Notations open Tacinterp open Libnames open Stdarg @@ -84,24 +83,24 @@ let fail_solver=tclFAIL 0 (Pp.str "GTauto failed") let gen_ground_tac flag taco ids bases = let backup= !qflag in Proofview.tclOR begin - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> qflag:=flag; let solver= match taco with Some tac-> tac | None-> snd (default_solver ()) in let startseq k = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let seq=empty_seq !ground_depth in let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in - Sigma.Unsafe.of_pair (k seq, sigma) - end } + tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq) + end in let result=ground_tac solver startseq in qflag := backup; result - end } + end end (fun (e, info) -> qflag := backup; Proofview.tclZERO ~info e) diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index ab1dd07c1..0fa3089e7 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -14,7 +14,6 @@ open Instances open Term open Tacmach.New open Tacticals.New -open Proofview.Notations let update_flags ()= let predref=ref Names.Cpred.empty in @@ -31,10 +30,10 @@ let update_flags ()= (Names.Id.Pred.full,Names.Cpred.complement !predref) let ground_tac solver startseq = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> update_flags (); let rec toptac skipped seq = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let () = if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 then @@ -127,7 +126,7 @@ let ground_tac solver startseq = end with Heap.EmptyHeap->solver end - end } in + end in let n = List.length (Proofview.Goal.hyps gl) in startseq (fun seq -> wrap n true (toptac []) seq) - end } + end diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 04bca584f..e1d765a42 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -21,7 +21,6 @@ open Formula open Sequent open Names open Misctypes -open Sigma.Notations open Context.Rel.Declaration let compare_instance inst1 inst2= @@ -114,9 +113,7 @@ let mk_open_instance env evmap id idc m t = let rec aux n avoid env evmap decls = if Int.equal n 0 then evmap, decls else let nid=(fresh_id_in_env avoid var_id env) in - let evmap = Sigma.Unsafe.of_evar_map evmap in - let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in - let evmap = Sigma.to_evar_map evmap in + let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in let decl = LocalAssum (Name nid, c) in aux (n-1) (nid::avoid) (EConstr.push_rel decl env) evmap (decl::decls) in let evmap, decls = aux m [] env evmap [] in @@ -126,7 +123,7 @@ let mk_open_instance env evmap id idc m t = let left_instance_tac (inst,id) continue seq= let open EConstr in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = project gl in match inst with Phantom dom-> @@ -137,10 +134,10 @@ let left_instance_tac (inst,id) continue seq= [tclTHENLIST [introf; (pf_constr_of_global id >>= fun idc -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let id0 = List.nth (pf_ids_of_hyps gl) 0 in generalize [mkApp(idc, [|mkVar id0|])] - end }); + end); introf; tclSOLVE [wrap 1 false continue (deepen (record (id,None) seq))]]; @@ -153,7 +150,7 @@ let left_instance_tac (inst,id) continue seq= let special_generalize= if m>0 then (pf_constr_of_global id >>= fun idc -> - Proofview.Goal.s_enter { s_enter = begin fun gl-> + Proofview.Goal.enter begin fun gl-> let (evmap, rc, ot) = mk_open_instance (pf_env gl) (project gl) id idc m t in let gt= it_mkLambda_or_LetIn @@ -162,8 +159,9 @@ let left_instance_tac (inst,id) continue seq= try Typing.type_of (pf_env gl) evmap gt with e when CErrors.noncritical e -> user_err Pp.(str "Untypable instance, maybe higher-order non-prenex quantification") in - Sigma.Unsafe.of_pair (generalize [gt], evmap) - end }) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evmap) + (generalize [gt]) + end) else pf_constr_of_global id >>= fun idc -> generalize [mkApp(idc,[|t|])] in @@ -172,20 +170,20 @@ let left_instance_tac (inst,id) continue seq= introf; tclSOLVE [wrap 1 false continue (deepen (record (id,Some c) seq))]] - end } + end let right_instance_tac inst continue seq= let open EConstr in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> match inst with Phantom dom -> tclTHENS (cut dom) [tclTHENLIST [introf; - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let id0 = List.nth (pf_ids_of_hyps gl) 0 in split (ImplicitBindings [mkVar id0]) - end }; + end; tclSOLVE [wrap 0 true continue (deepen seq)]]; tclTRY assumption] | Real ((0,t),_) -> @@ -193,7 +191,7 @@ let right_instance_tac inst continue seq= (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> tclFAIL 0 (Pp.str "not implemented ... yet") - end } + end let instance_tac inst= if (snd inst)==dummy_id then @@ -202,9 +200,9 @@ let instance_tac inst= left_instance_tac inst let quantified_tac lf backtrack continue seq = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let insts=give_instances (project gl) lf seq in tclORELSE (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts)) backtrack - end } + end diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index f745dbeb4..b7fe25a32 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -32,7 +32,7 @@ type lseqtac= global_reference -> seqtac type 'a with_backtracking = tactic -> 'a let wrap n b continue seq = - Proofview.Goal.nf_enter { enter = begin fun gls -> + Proofview.Goal.nf_enter begin fun gls -> Control.check_for_interrupt (); let nc = Proofview.Goal.hyps gls in let env=pf_env gls in @@ -52,7 +52,7 @@ let wrap n b continue seq = let seq2=if b then add_formula env sigma Concl dummy_id (pf_concl gls) seq1 else seq1 in continue seq2 - end } + end let basename_of_global=function VarRef id->id @@ -65,12 +65,12 @@ let clear_global=function (* connection rules *) let axiom_tac t seq = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> try pf_constr_of_global (find_left (project gl) t seq) >>= fun c -> exact_no_check c with Not_found -> tclFAIL 0 (Pp.str "No axiom link") - end } + end let ll_atom_tac a backtrack id continue seq = let open EConstr in @@ -107,7 +107,7 @@ let arrow_tac backtrack continue seq= (* left connectives rules *) let left_and_tac ind backtrack id continue seq = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let n=(construct_nhyps (pf_env gl) ind).(0) in tclIFTHENELSE (tclTHENLIST @@ -116,10 +116,10 @@ let left_and_tac ind backtrack id continue seq = tclDO n intro]) (wrap n false continue seq) backtrack - end } + end let left_or_tac ind backtrack id continue seq = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let v=construct_nhyps (pf_env gl) ind in let f n= tclTHENLIST @@ -130,7 +130,7 @@ let left_or_tac ind backtrack id continue seq = (pf_constr_of_global id >>= simplest_elim) (Array.map f v) backtrack - end } + end let left_false_tac id= Tacticals.New.pf_constr_of_global id >>= simplest_elim @@ -140,7 +140,7 @@ let left_false_tac id= (* We use this function for false, and, or, exists *) let ll_ind_tac (ind,u as indu) largs backtrack id continue seq = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let rcs=ind_hyps (pf_env gl) (project gl) 0 indu largs in let vargs=Array.of_list largs in (* construire le terme H->B, le generaliser etc *) @@ -161,7 +161,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq = clear_global id; tclDO lp intro]) (wrap lp false continue seq) backtrack - end } + end let ll_arrow_tac a b c backtrack id continue seq= let open EConstr in @@ -199,7 +199,7 @@ let forall_tac backtrack continue seq= backtrack) let left_exists_tac ind backtrack id continue seq = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let n=(construct_nhyps (pf_env gl) ind).(0) in tclIFTHENELSE (Tacticals.New.pf_constr_of_global id >>= simplest_elim) @@ -207,7 +207,7 @@ let left_exists_tac ind backtrack id continue seq = tclDO n intro; (wrap (n-1) false continue seq)]) backtrack - end } + end let ll_forall_tac prod backtrack id continue seq= tclORELSE @@ -215,12 +215,12 @@ let ll_forall_tac prod backtrack id continue seq= [tclTHENLIST [intro; (pf_constr_of_global id >>= fun idc -> - Proofview.Goal.enter { enter = begin fun gls-> + Proofview.Goal.enter begin fun gls-> let open EConstr in let id0 = List.nth (pf_ids_of_hyps gls) 0 in let term=mkApp(idc,[|mkVar(id0)|]) in tclTHEN (generalize [term]) (clear [id0]) - end }); + end); clear_global id; intro; tclCOMPLETE (wrap 1 false continue (deepen seq))]; @@ -239,9 +239,9 @@ let defined_connectives=lazy AllOccurrences,EvalConstRef (fst (Term.destConst (constant "iff")))] let normalize_evaluables= - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> unfold_in_concl (Lazy.force defined_connectives) <*> tclMAP (fun id -> unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)) (pf_ids_of_hyps gl) - end } + end diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index a6290cb00..317444cf1 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -469,7 +469,7 @@ exception GoalDone (* Résolution d'inéquations linéaires dans R *) let rec fourier () = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; @@ -633,7 +633,7 @@ let rec fourier () = (* ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *) !tac (* ((tclABSTRACT None !tac) gl) *) - end } + end ;; (* diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index c2f705898..fd4962398 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1481,7 +1481,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = tclCOMPLETE( Eauto.eauto_with_bases (true,5) - [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}] + [(fun _ sigma -> (sigma, Lazy.force refl_equal))] [Hints.Hint_db.empty empty_transparent_state false] ) ) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index a0eb9e2b2..b8070ff88 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -12,7 +12,6 @@ open Context.Rel.Declaration open Indfun_common open Functional_principles_proofs open Misctypes -open Sigma.Notations module RelDecl = Context.Rel.Declaration @@ -669,11 +668,9 @@ let build_case_scheme fa = let ind = first_fun_kn,funs_indexes in (ind,Univ.Instance.empty)(*FIXME*),prop_sort in - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (scheme, sigma, _) = + let (sigma, scheme) = Indrec.build_case_analysis_scheme_default env sigma ind sf in - let sigma = Sigma.to_evar_map sigma in let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in let sorts = (fun (_,_,x) -> diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index bd2ac8c67..d28e0aba0 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -37,9 +37,10 @@ let pr_fun_ind_using_typed prc prlc _ opt_c = match opt_c with | None -> mt () | Some b -> - let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in + let (_, b) = b (Global.env ()) Evd.empty in spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b) + ARGUMENT EXTEND fun_ind_using TYPED AS constr_with_bindings option PRINTED BY pr_fun_ind_using_typed diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index a23c51495..f1a9758e8 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -11,7 +11,6 @@ open Glob_term open Declarations open Misctypes open Decl_kinds -open Sigma.Notations module RelDecl = Context.Rel.Declaration @@ -93,7 +92,7 @@ let functional_induction with_clean c princl pat = in let encoded_pat_as_patlist = List.make (List.length args + List.length c_list - 1) None @ [pat] in - List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None)) + List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)) )),(None,pat),None)) (args@c_list) encoded_pat_as_patlist in let princ' = Some (princ,bindings) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index e6f199dba..ff397d2e9 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -42,7 +42,6 @@ open Auto open Eauto open Indfun_common -open Sigma.Notations open Context.Rel.Declaration (* Ugly things which should not be here *) @@ -700,11 +699,9 @@ let mkDestructEq : observe_tclTHENLIST (str "mkDestructEq") [Proofview.V82.of_tactic (generalize new_hyps); (fun g2 -> - let changefun patvars = { run = fun sigma -> - let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in - let Sigma (c, sigma, p) = redfun.Reductionops.e_redfun (pf_env g2) sigma (pf_concl g2) in - Sigma (c, sigma, p) - } in + let changefun patvars sigma = + pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) + in Proofview.V82.of_tactic (change_in_concl None changefun) g2); Proofview.V82.of_tactic (simplest_case expr)]), to_revert @@ -1357,7 +1354,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp (Proofview.V82.of_tactic e_assumption); Eauto.eauto_with_bases (true,5) - [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}] + [(fun _ sigma -> (sigma, (Lazy.force refl_equal)))] [Hints.Hint_db.empty empty_transparent_state false] ] ) diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 0a13a20a9..ea1660d90 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -16,8 +16,6 @@ open Genredexpr open Stdarg open Extraargs -open Sigma.Notations - DECLARE PLUGIN "coretactics" (** Basic tactics *) @@ -160,12 +158,12 @@ END (** Split *) let rec delayed_list = function -| [] -> { Tacexpr.delayed = fun _ sigma -> Sigma.here [] sigma } +| [] -> fun _ sigma -> (sigma, []) | x :: l -> - { Tacexpr.delayed = fun env sigma -> - let Sigma (x, sigma, p) = x.Tacexpr.delayed env sigma in - let Sigma (l, sigma, q) = (delayed_list l).Tacexpr.delayed env sigma in - Sigma (x :: l, sigma, p +> q) } + fun env sigma -> + let (sigma, x) = x env sigma in + let (sigma, l) = delayed_list l env sigma in + (sigma, x :: l) TACTIC EXTEND split [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ] diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index bf84f61a5..7db484d82 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -16,8 +16,6 @@ open Tacexpr open Refiner open Evd open Locus -open Sigma.Notations -open Proofview.Notations open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -81,7 +79,7 @@ let instantiate_tac_by_name id c = let let_evar name typ = let src = (Loc.tag Evar_kinds.GoalEvar) in - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let sigma = ref sigma in @@ -93,17 +91,14 @@ let let_evar name typ = Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env)) | Names.Name id -> id in - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in - let tac = - (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere) - in - Sigma (tac, sigma, p) - end } + let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere) + end let hget_evar n = let open EConstr in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in let evl = evar_list sigma concl in @@ -113,5 +108,5 @@ let hget_evar n = let ev = List.nth evl (n-1) in let ev_type = EConstr.existential_type sigma ev in Tactics.change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl)) - end } + end diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 9726a5b40..8afe3053d 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -24,7 +24,6 @@ open Util open Termops open Equality open Misctypes -open Sigma.Notations open Proofview.Notations DECLARE PLUGIN "extratactics" @@ -80,12 +79,12 @@ let induction_arg_of_quantified_hyp = function ElimOnIdent and not as "constr" *) let mytclWithHoles tac with_evars c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Tacmach.New.pf_env gl in let sigma = Tacmach.New.project gl in let sigma',c = Tactics.force_destruction_arg with_evars env sigma c in Tacticals.New.tclWITHHOLES with_evars (tac with_evars (Some c)) sigma' - end } + end let elimOnConstrWithHoles tac with_evars c = Tacticals.New.tclDELAYEDWITHHOLES with_evars c @@ -115,7 +114,7 @@ END let discrHyp id = Proofview.tclEVARMAP >>= fun sigma -> - discr_main { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma } + discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) let injection_main with_evars c = elimOnConstrWithHoles (injClause None) with_evars c @@ -147,7 +146,7 @@ END let injHyp id = Proofview.tclEVARMAP >>= fun sigma -> - injection_main false { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma } + injection_main false (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) TACTIC EXTEND dependent_rewrite | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ] @@ -354,23 +353,22 @@ let constr_flags () = { Pretyping.expand_evars = true } let refine_tac ist simple with_classes c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let flags = { constr_flags () with Pretyping.use_typeclasses = with_classes } in let expected_type = Pretyping.OfType concl in let c = Pretyping.type_uconstr ~flags ~expected_type ist c in - let update = { run = fun sigma -> - let Sigma (c, sigma, p) = c.delayed env sigma in - Sigma (c, sigma, p) - } in + let update = begin fun sigma -> + c env sigma + end in let refine = Refine.refine ~unsafe:true update in if simple then refine else refine <*> Tactics.New.reduce_after_refine <*> Proofview.shelve_unifiable - end } + end TACTIC EXTEND refine | [ "refine" uconstr(c) ] -> @@ -663,9 +661,8 @@ let subst_hole_with_term occ tc t = open Tacmach let hResolve id c occ t = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let sigma = Sigma.to_evar_map sigma in let env = Termops.clear_named_body id (Proofview.Goal.env gl) in let concl = Proofview.Goal.concl gl in let env_ids = Termops.ids_of_context env in @@ -684,11 +681,9 @@ let hResolve id c occ t = let t_constr = EConstr.of_constr t_constr in let sigma = Evd.merge_universe_context sigma ctx in let t_constr_type = Retyping.get_type_of env sigma t_constr in - let tac = + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,concl))) - in - Sigma.Unsafe.of_pair (tac, sigma) - end } + end let hResolve_auto id c t = let rec resolve_auto n = @@ -726,12 +721,12 @@ END exception Found of unit Proofview.tactic let rewrite_except h = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.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 = @@ -745,29 +740,29 @@ 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.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req -> Tacticals.New.tclTHENLIST [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))]; - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in (** FIXME: this looks really wrong. Does anybody really use this tactic? *) - let Sigma (c, _, _) = (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a]).Reductionops.e_redfun env (Sigma.Unsafe.of_evar_map Evd.empty) concl in + let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl in change_concl c - end }; + end; simplest_case a] - end } + end let case_eq_intros_rewrite x = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let n = nb_prod (Tacmach.New.project gl) (Proofview.Goal.concl gl) in (* Pp.msgnl (Printer.pr_lconstr x); *) Tacticals.New.tclTHENLIST [ mkCaseEq x; - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.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 (Tacmach.New.project gl) concl in @@ -776,9 +771,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 sigma t = let cl = induction_arg_of_quantified_hyp (NamedHyp (Id.of_string "x")) in @@ -802,15 +797,15 @@ let destauto t = with Found tac -> tac let destauto_in id = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in (* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) (* Pp.msgnl (Printer.pr_lconstr (ctype)); *) destauto ctype - end } + end TACTIC EXTEND destauto -| [ "destauto" ] -> [ Proofview.Goal.enter { enter = begin fun gl -> destauto (Proofview.Goal.concl gl) end } ] +| [ "destauto" ] -> [ Proofview.Goal.enter begin fun gl -> destauto (Proofview.Goal.concl gl) end ] | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ] END @@ -822,21 +817,21 @@ END (**********************************************************************) TACTIC EXTEND transparent_abstract -| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter { enter = fun gl -> - Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) } ] -| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter { enter = fun gl -> - Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) } ] +| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter begin fun gl -> + Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end ] +| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter begin fun gl -> + Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end ] END (* ********************************************************************* *) let eq_constr x y = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let evd = Tacmach.New.project gl in match EConstr.eq_constr_universes evd x y with | Some _ -> Proofview.tclUNIT () | None -> Tacticals.New.tclFAIL 0 (str "Not equal") - end } + end TACTIC EXTEND constr_eq | [ "constr_eq" constr(x) constr(y) ] -> [ eq_constr x y ] @@ -1082,7 +1077,7 @@ TACTIC EXTEND guard END let decompose l c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let to_ind c = if isInd sigma c then fst (destInd sigma c) @@ -1090,7 +1085,7 @@ let decompose l c = 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/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 50e8255a6..2c2a4b850 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -15,7 +15,6 @@ open Pcoq.Prim open Pcoq.Constr open Pltac open Hints -open Tacexpr open Names DECLARE PLUGIN "g_auto" @@ -49,10 +48,7 @@ let eval_uconstrs ist cs = fail_evar = false; expand_evars = true } in - let map c = { delayed = fun env sigma -> - let Sigma.Sigma (c, sigma, p) = c.delayed env sigma in - Sigma.Sigma (c, sigma, p) - } in + let map c env sigma = c env sigma in List.map (fun c -> map (Pretyping.type_uconstr ~flags ist c)) cs let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index 23ce368ee..dd5307638 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -102,18 +102,18 @@ let rec eq_constr_mod_evars sigma x y = | _, _ -> compare_constr sigma (fun x y -> eq_constr_mod_evars sigma x y) x y let progress_evars t = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let check = - Proofview.Goal.enter { enter = begin fun gl' -> + Proofview.Goal.enter begin fun gl' -> let sigma = Tacmach.New.project gl' in let newconcl = Proofview.Goal.concl gl' in if eq_constr_mod_evars sigma concl newconcl then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)") else Proofview.tclUNIT () - end } + end in t <*> check - end } + end TACTIC EXTEND progress_evars [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.tactic_of_value ist t) ] diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 5adf8475a..25258ffa9 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -18,7 +18,6 @@ open Glob_term open Geninterp open Extraargs open Tacmach -open Proofview.Notations open Rewrite open Stdarg open Pcoq.Vernac_ @@ -123,7 +122,7 @@ TACTIC EXTEND rewrite_strat END let clsubstitute o c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id' } when Id.equal id' id -> true | _ -> false in let hyps = Tacmach.New.pf_ids_of_hyps gl in Tacticals.New.tclMAP @@ -132,7 +131,7 @@ let clsubstitute o c = | Some id when is_tac id -> Tacticals.New.tclIDTAC | _ -> cl_rewrite_clause c o AllOccurrences cl) (None :: List.map (fun id -> Some id) hyps) - end } + end TACTIC EXTEND substitute | [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ] diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 902985827..9446f9df4 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1179,11 +1179,10 @@ let declare_extra_genarg_pprule wit (** Registering *) -let run_delayed c = - Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma } +let run_delayed c = c (Global.env ()) Evd.empty let run_delayed_destruction_arg = function (* HH: Using Evd.empty looks suspicious *) - | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (fst (run_delayed g)) + | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (snd (run_delayed g)) | clear_flag,ElimOnAnonHyp n as x -> x | clear_flag,ElimOnIdent id as x -> x @@ -1203,7 +1202,7 @@ let () = wit_intro_pattern (Miscprint.pr_intro_pattern pr_constr_expr) (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) - (Miscprint.pr_intro_pattern (fun c -> pr_econstr (fst (run_delayed c)))); + (Miscprint.pr_intro_pattern (fun c -> pr_econstr (snd (run_delayed c)))); Genprint.register_print0 wit_clause_dft_concl (pr_clauses (Some true) pr_lident) @@ -1236,11 +1235,11 @@ let () = Genprint.register_print0 wit_bindings (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (fst (run_delayed it))); + (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (snd (run_delayed it))); Genprint.register_print0 wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_with_bindings pr_econstr pr_leconstr (fst (run_delayed it))); + (fun it -> pr_with_bindings pr_econstr pr_leconstr (snd (run_delayed it))); Genprint.register_print0 Tacarg.wit_destruction_arg (pr_destruction_arg pr_constr_expr pr_lconstr_expr) (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index f028abde9..68dc1fd37 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -33,7 +33,6 @@ open Environ open Termops open EConstr open Libnames -open Sigma.Notations open Proofview.Notations open Context.Named.Declaration @@ -66,9 +65,7 @@ type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *) let find_global dir s = let gr = lazy (find_reference dir s) in fun (evd,cstrs) -> - let sigma = Sigma.Unsafe.of_evar_map evd in - let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force gr) in - let evd = Sigma.to_evar_map sigma in + let (evd, c) = Evarutil.new_global evd (Lazy.force gr) in (evd, cstrs), c (** Utility for dealing with polymorphic applications *) @@ -89,9 +86,7 @@ let cstrevars evars = snd evars let new_cstr_evar (evd,cstrs) env t = let s = Typeclasses.set_resolvable Evd.Store.empty false in - let evd = Sigma.Unsafe.of_evar_map evd in - let Sigma (t, evd', _) = Evarutil.new_evar ~store:s env evd t in - let evd' = Sigma.to_evar_map evd' in + let (evd', t) = Evarutil.new_evar ~store:s env evd t in let ev, _ = destEvar evd' t in (evd', Evar.Set.add ev cstrs), t @@ -176,17 +171,13 @@ end) = struct let proper_type = let l = lazy (Lazy.force proper_class).cl_impl in fun (evd,cstrs) -> - let sigma = Sigma.Unsafe.of_evar_map evd in - let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in - let evd = Sigma.to_evar_map sigma in + let (evd, c) = Evarutil.new_global evd (Lazy.force l) in (evd, cstrs), c let proper_proxy_type = let l = lazy (Lazy.force proper_proxy_class).cl_impl in fun (evd,cstrs) -> - let sigma = Sigma.Unsafe.of_evar_map evd in - let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in - let evd = Sigma.to_evar_map sigma in + let (evd, c) = Evarutil.new_global evd (Lazy.force l) in (evd, cstrs), c let proper_proof env evars carrier relation x = @@ -357,9 +348,7 @@ end) = struct (try let params, args = Array.chop (Array.length args - 2) args in let env' = push_rel_context rels env in - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma ((evar, _), evars, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in - let evars = Sigma.to_evar_map evars in + let (evars, (evar, _)) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in let evars, inst = app_poly env (evars,Evar.Set.empty) rewrite_relation_class [| evar; mkApp (c, params) |] in @@ -419,9 +408,7 @@ module TypeGlobal = struct let inverse env (evd,cstrs) car rel = - let sigma = Sigma.Unsafe.of_evar_map evd in - let Sigma (sort, sigma, _) = Evarutil.new_Type ~rigid:Evd.univ_flexible env sigma in - let evd = Sigma.to_evar_map sigma in + let (evd, sort) = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |] end @@ -751,9 +738,9 @@ let default_flags = { under_lambdas = true; on_morphisms = true; } let get_opt_rew_rel = function RewPrf (rel, prf) -> Some rel | _ -> None -let new_global (evars, cstrs) gr = - let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map evars) gr - in (Sigma.to_evar_map sigma, cstrs), c +let new_global (evars, cstrs) gr = + let (sigma,c) = Evarutil.new_global evars gr in + (sigma, cstrs), c let make_eq sigma = new_global sigma (Coqlib.build_coq_eq ()) @@ -1406,15 +1393,14 @@ module Strategies = let reduce (r : Redexpr.red_expr) : 'a pure_strategy = { strategy = fun { state = state ; env = env ; term1 = t ; ty1 = ty ; cstr = cstr ; evars = evars } -> let rfn, ckind = Redexpr.reduction_of_red_expr env r in - let sigma = Sigma.Unsafe.of_evar_map (goalevars evars) in - let Sigma (t', sigma, _) = rfn.Reductionops.e_redfun env sigma t in - let evars' = Sigma.to_evar_map sigma in - if Termops.eq_constr evars' t' t then + let sigma = goalevars evars in + let (sigma, t') = rfn env sigma t in + if Termops.eq_constr sigma t' t then state, Identity else state, Success { rew_car = ty; rew_from = t; rew_to = t'; rew_prf = RewCast ckind; - rew_evars = evars', cstrevars evars } + rew_evars = sigma, cstrevars evars } } let fold_glob c : 'a pure_strategy = { strategy = @@ -1541,7 +1527,7 @@ let rec insert_dependent env sigma decl accu hyps = match hyps with insert_dependent env sigma decl (ndecl :: accu) rem let assert_replacing id newt tac = - let prf = Proofview.Goal.enter { enter = begin fun gl -> + let prf = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -1552,17 +1538,17 @@ let assert_replacing id newt tac = | d :: rem -> insert_dependent env sigma (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in - Refine.refine ~unsafe:false { run = begin fun sigma -> - let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in - let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in + Refine.refine ~unsafe:false begin fun sigma -> + let (sigma, ev) = Evarutil.new_evar env' sigma concl in + let (sigma, ev') = Evarutil.new_evar env sigma newt in let map d = let n = NamedDecl.get_id d in if Id.equal n id then ev' else mkVar n in - let (e, _) = destEvar (Sigma.to_evar_map sigma) ev in - Sigma (mkEvar (e, Array.map_of_list map nc), sigma, p +> q) - end } - end } in + let (e, _) = destEvar sigma ev in + (sigma, mkEvar (e, Array.map_of_list map nc)) + end + end in Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac) let newfail n s = @@ -1586,7 +1572,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = match clause, prf with | Some id, Some p -> let tac = tclTHENLIST [ - Refine.refine ~unsafe:false { run = fun h -> Sigma.here p h }; + Refine.refine ~unsafe:false (fun h -> (h,p)); Proofview.Unsafe.tclNEWGOALS gls; ] in Proofview.Unsafe.tclEVARS undef <*> @@ -1597,19 +1583,19 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = beta_hyp id | None, Some p -> Proofview.Unsafe.tclEVARS undef <*> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.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 + let make = begin fun sigma -> + let (sigma, ev) = Evarutil.new_evar env sigma newt in + (sigma, mkApp (p, [| ev |])) + end in Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls - end } + end | None, None -> Proofview.Unsafe.tclEVARS undef <*> convert_concl_no_check newt DEFAULTcast in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -1637,7 +1623,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress 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 (); Proofview.tclUNIT () @@ -2092,7 +2078,7 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } (** Setoid rewriting when called with "rewrite" *) let general_s_rewrite cl l2r occs (c,l) ~new_goals = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in let unify env evars t = unify_abs res l2r sort env evars t in let app = apply_rule unify occs in @@ -2114,7 +2100,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals = | RewriteFailure e -> tclFAIL 0 (str"setoid rewrite failed: " ++ e) | e -> Proofview.tclZERO ~info e) - end } + end let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite @@ -2126,7 +2112,7 @@ let not_declared env sigma ty rel = str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library") let setoid_proof ty fn fallback = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in @@ -2155,7 +2141,7 @@ let setoid_proof ty fn fallback = | e' -> Proofview.tclZERO ~info e' end end - end } + end let tac_open ((evm,_), c) tac = (tclTHEN (Proofview.Unsafe.tclEVARS evm) (tac c)) @@ -2195,7 +2181,7 @@ let setoid_transitivity c = let setoid_symmetry_in id = let open Tacmach.New in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = project gl in let ctype = pf_unsafe_type_of gl (mkVar id) in let binders,concl = decompose_prod_assum sigma ctype in @@ -2212,7 +2198,7 @@ let setoid_symmetry_in id = (tclTHENLAST (Tactics.assert_after_replacing id new_hyp) (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ])) - end } + end let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index b78dc3742..cfb698cd8 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -117,8 +117,7 @@ type open_glob_constr = unit * glob_constr_and_expr type binding_bound_vars = Constr_matching.binding_bound_vars type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern -type 'a delayed_open = 'a Tactypes.delayed_open = - { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } +type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 37fdd185e..ff76d06cf 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -37,7 +37,6 @@ open Misctypes open Locus open Tacintern open Taccoerce -open Sigma.Notations open Proofview.Notations open Context.Named.Declaration @@ -767,9 +766,7 @@ let interp_may_eval f ist env sigma = function let (sigma,redexp) = interp_red_expr ist env sigma r in let (sigma,c_interp) = f ist env sigma c in let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (c, sigma, _) = redfun.Reductionops.e_redfun env sigma c_interp in - (Sigma.to_evar_map sigma, c) + redfun env sigma c_interp | ConstrContext ((loc,s),c) -> (try let (sigma,ic) = f ist env sigma c in @@ -829,12 +826,12 @@ let rec message_of_value v = Ftactic.return (str "<tactic>") else if has_type v (topwit wit_constr) then let v = out_gen (topwit wit_constr) v in - Ftactic.enter {enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end } + Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end else if has_type v (topwit wit_constr_under_binders) then let c = out_gen (topwit wit_constr_under_binders) v in - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> Ftactic.return (pr_constr_under_binders_env (pf_env gl) (project gl) c) - end } + end else if has_type v (topwit wit_unit) then Ftactic.return (str "()") else if has_type v (topwit wit_int) then @@ -842,24 +839,24 @@ let rec message_of_value v = else if has_type v (topwit wit_intro_pattern) then let p = out_gen (topwit wit_intro_pattern) v in let print env sigma c = - let (c, sigma) = Tactics.run_delayed env sigma c in + let (sigma, c) = c env sigma in pr_econstr_env env sigma c in - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p) - end } + end else if has_type v (topwit wit_constr_context) then let c = out_gen (topwit wit_constr_context) v in - Ftactic.enter { enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end } + Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end else if has_type v (topwit wit_uconstr) then let c = out_gen (topwit wit_uconstr) v in - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> Ftactic.return (pr_closed_glob_env (pf_env gl) (project gl) c) - end } + end else if has_type v (topwit wit_var) then let id = out_gen (topwit wit_var) v in - Ftactic.enter { enter = begin fun gl -> Ftactic.return (pr_id id) end } + Ftactic.enter begin fun gl -> Ftactic.return (pr_id id) end else match Value.to_list v with | Some l -> Ftactic.List.map message_of_value l >>= fun l -> @@ -905,11 +902,7 @@ and interp_intro_pattern_action ist env sigma = function let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in sigma, IntroInjection l | IntroApplyOn ((loc,c),ipat) -> - let c = { delayed = fun env sigma -> - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = interp_open_constr ist env sigma c in - Sigma.Unsafe.of_pair (c, sigma) - } in + let c env sigma = interp_open_constr ist env sigma c in let sigma,ipat = interp_intro_pattern ist env sigma ipat in sigma, IntroApplyOn ((loc,c),ipat) | IntroWildcard | IntroRewrite _ as x -> sigma, x @@ -1003,21 +996,15 @@ let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) = let loc1 = loc_of_glob_constr c in let loc2 = loc_of_bindings bl in let loc = Loc.merge_opt loc1 loc2 in - let f = { delayed = fun env sigma -> - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = interp_open_constr_with_bindings ist env sigma cb in - Sigma.Unsafe.of_pair (c, sigma) - } in - (loc,f) + let f env sigma = interp_open_constr_with_bindings ist env sigma cb in + (loc,f) let interp_destruction_arg ist gl arg = match arg with | keep,ElimOnConstr c -> - keep,ElimOnConstr { delayed = fun env sigma -> - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = interp_open_constr_with_bindings ist env sigma c in - Sigma.Unsafe.of_pair (c, sigma) - } + keep,ElimOnConstr begin fun env sigma -> + interp_open_constr_with_bindings ist env sigma c + end | keep,ElimOnAnonHyp n as x -> x | keep,ElimOnIdent (loc,id) -> let error () = user_err ?loc @@ -1028,12 +1015,12 @@ let interp_destruction_arg ist gl arg = if Tactics.is_quantified_hypothesis id' gl then keep,ElimOnIdent (loc,id') else - (keep, ElimOnConstr { delayed = begin fun env sigma -> - try Sigma.here (constr_of_id env id', NoBindings) sigma + (keep, ElimOnConstr begin fun env sigma -> + try (sigma, (constr_of_id env id', NoBindings)) with Not_found -> user_err ?loc ~hdr:"interp_destruction_arg" ( pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.") - end }) + end) in try (** FIXME: should be moved to taccoerce *) @@ -1051,18 +1038,17 @@ let interp_destruction_arg ist gl arg = keep,ElimOnAnonHyp (out_gen (topwit wit_int) v) else match Value.to_constr v with | None -> error () - | Some c -> keep,ElimOnConstr { delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) } + | Some c -> keep,ElimOnConstr (fun env sigma -> (sigma, (c,NoBindings))) with Not_found -> (* We were in non strict (interactive) mode *) if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (loc,id) else let c = (CAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in - let f = { delayed = fun env sigma -> - let sigma = Sigma.to_evar_map sigma in + let f env sigma = let (sigma,c) = interp_open_constr ist env sigma c in - Sigma.Unsafe.of_pair ((c,NoBindings), sigma) - } in + (sigma, (c,NoBindings)) + in keep,ElimOnConstr f (* Associates variables with values and gives the remaining variables and @@ -1198,9 +1184,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.enter { enter = begin fun gl -> Tactics.tclABSTRACT + Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac) - end } + end | TacThen (t1,t) -> Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t) | TacDispatch tl -> @@ -1318,12 +1304,13 @@ and interp_tacarg ist arg : Val.t Ftactic.t = | TacGeneric arg -> interp_genarg ist arg | Reference r -> interp_ltac_reference false ist r | ConstrMayEval c -> - Ftactic.s_enter { s_enter = begin fun gl -> + Ftactic.enter begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in - Sigma.Unsafe.of_pair (Ftactic.return (Value.of_constr c_interp), sigma) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Ftactic.return (Value.of_constr c_interp)) + end | TacCall (loc,(r,[])) -> interp_ltac_reference true ist r | TacCall (loc,(f,l)) -> @@ -1332,18 +1319,19 @@ and interp_tacarg ist arg : Val.t Ftactic.t = Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs -> interp_app loc ist fv largs | TacFreshId l -> - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> let id = interp_fresh_id ist (pf_env gl) (project gl) l in Ftactic.return (in_gen (topwit wit_intro_pattern) (Loc.tag @@ IntroNaming (IntroIdentifier id))) - end } + end | TacPretype c -> - Ftactic.s_enter { s_enter = begin fun gl -> + Ftactic.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let c = interp_uconstr ist env (Sigma.to_evar_map sigma) c in - let Sigma (c, sigma, p) = (type_uconstr ist c).delayed env sigma in - Sigma (Ftactic.return (Value.of_constr c), sigma, p) - end } + let c = interp_uconstr ist env sigma c in + let (sigma, c) = type_uconstr ist c env sigma in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Ftactic.return (Value.of_constr c)) + end | TacNumgoals -> Ftactic.lift begin let open Proofview.Notations in @@ -1504,16 +1492,16 @@ and interp_match ist lz constr lmr = Proofview.tclZERO ~info e end end >>= fun constr -> - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in interp_match_successes lz ist (Tactic_matching.match_term env sigma constr ilr) - end } + end (* Interprets the Match Context expressions *) and interp_match_goal ist lz lr lmr = - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in let hyps = Proofview.Goal.hyps gl in @@ -1521,7 +1509,7 @@ and interp_match_goal ist lz lr lmr = let concl = Proofview.Goal.concl gl in let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in interp_match_successes lz ist (Tactic_matching.match_goal env sigma hyps concl ilr) - end } + end (* Interprets extended tactic generic arguments *) and interp_genarg ist x : Val.t Ftactic.t = @@ -1558,24 +1546,25 @@ and interp_genarg ist x : Val.t Ftactic.t = independently of goals. *) and interp_genarg_constr_list ist x = - Ftactic.nf_s_enter { s_enter = begin fun gl -> + Ftactic.nf_enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let sigma = Proofview.Goal.sigma gl in let lc = Genarg.out_gen (glbwit (wit_list wit_constr)) x in let (sigma,lc) = interp_constr_list ist env sigma lc in let lc = in_list (val_tag wit_constr) lc in - Sigma.Unsafe.of_pair (Ftactic.return lc, sigma) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Ftactic.return lc) + end and interp_genarg_var_list ist x = - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let sigma = Proofview.Goal.sigma gl in let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in let lc = interp_hyp_list ist env sigma lc in let lc = in_list (val_tag wit_var) lc in Ftactic.return lc - end } + end (* Interprets tactic expressions : returns a "constr" *) and interp_ltac_constr ist e : EConstr.t Ftactic.t = @@ -1584,7 +1573,7 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t = (val_interp ist e) begin function (err, info) -> match err with | Not_found -> - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in Proofview.tclLIFT begin debugging_step ist (fun () -> @@ -1592,11 +1581,11 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t = Pptactic.pr_glob_tactic env e) end <*> Proofview.tclZERO Not_found - end } + end | err -> Proofview.tclZERO ~info err end end >>= fun result -> - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let result = Value.normalize result in @@ -1613,7 +1602,7 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t = let env = Proofview.Goal.env gl in Tacticals.New.tclZEROMSG (str "Must evaluate to a closed term" ++ fnl() ++ str "offending expression: " ++ fnl() ++ pr_inspect env e result) - end } + end (* Interprets tactic expressions : returns a "tactic" *) @@ -1635,7 +1624,7 @@ and interp_atomic ist tac : unit Proofview.tactic = match tac with (* Basic tactics *) | TacIntroPattern (ev,l) -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in @@ -1645,11 +1634,11 @@ and interp_atomic ist tac : unit Proofview.tactic = (* spiwack: print uninterpreted, not sure if it is the expected behaviour. *) (Tactics.intro_patterns ev l')) sigma - end } + end | 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 { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let l = List.map (fun (k,c) -> @@ -1662,10 +1651,10 @@ and interp_atomic ist tac : unit Proofview.tactic = let sigma,(id,cl) = interp_in_hyp_as ist env sigma cl in sigma, Tactics.apply_delayed_in a ev id l cl in Tacticals.New.tclWITHHOLES ev tac sigma - end } + end end | TacElim (ev,(keep,cb),cbo) -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in @@ -1675,9 +1664,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 { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in @@ -1686,11 +1675,11 @@ 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 | TacMutualFix (id,n,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let env = pf_env gl in let f sigma (id,n,c) = let (sigma,c_interp) = interp_type ist env sigma c in @@ -1698,14 +1687,14 @@ and interp_atomic ist tac : unit Proofview.tactic = let (sigma,l_interp) = Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) in - let tac = Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0 in - Sigma.Unsafe.of_pair (tac, sigma) - end } + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0) + end end | TacMutualCofix (id,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let env = pf_env gl in let f sigma (id,c) = let (sigma,c_interp) = interp_type ist env sigma c in @@ -1713,12 +1702,12 @@ and interp_atomic ist tac : unit Proofview.tactic = let (sigma,l_interp) = Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) in - let tac = Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0 in - Sigma.Unsafe.of_pair (tac, sigma) - end } + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0) + end end | TacAssert (ev,b,t,ipat,c) -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let (sigma,c) = @@ -1733,9 +1722,9 @@ and interp_atomic ist tac : unit Proofview.tactic = (name_atomic ~env (TacAssert(ev,b,Option.map (Option.map ignore) t,ipat,c)) (Tactics.forward b tac ipat' c)) sigma - end } + end | TacGeneralize cl -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = project 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 @@ -1743,9 +1732,9 @@ and interp_atomic ist tac : unit Proofview.tactic = (name_atomic ~env (TacGeneralize cl) (Tactics.generalize_gen cl)) sigma - end } + end | TacLetTac (ev,na,c,clp,b,eqpat) -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let clp = interp_clause ist env sigma clp in @@ -1777,13 +1766,13 @@ and interp_atomic ist tac : unit Proofview.tactic = (Tacticals.New.tclWITHHOLES ev (let_pat_tac b (interp_name ist env sigma na) (sigma,c) clp eqpat) sigma') - end } + end (* Derived basic tactics *) | TacInductionDestruct (isrec,ev,(l,el)) -> (* spiwack: some unknown part of destruct needs the goal to be prenormalised. *) - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let sigma,l = @@ -1802,23 +1791,23 @@ and interp_atomic ist tac : unit Proofview.tactic = let l,lp = List.split l in let sigma,el = Option.fold_map (interp_open_constr_with_bindings ist env) sigma el in - let tac = name_atomic ~env + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (name_atomic ~env (TacInductionDestruct(isrec,ev,(lp,el))) - (Tactics.induction_destruct isrec ev (l,el)) - in - Sigma.Unsafe.of_pair (tac, sigma) - end } + (Tactics.induction_destruct isrec ev (l,el))) + end (* Conversion *) | TacReduce (r,cl) -> - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in - Sigma.Unsafe.of_pair (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl), sigma) - end } + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl)) + end | TacChange (None,c,cl) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let is_onhyps = match cl.onhyps with | None | Some [] -> true | _ -> false @@ -1827,58 +1816,50 @@ and interp_atomic ist tac : unit Proofview.tactic = | AllOccurrences | NoOccurrences -> true | _ -> false in - let c_interp patvars = { Sigma.run = begin fun sigma -> + let c_interp patvars sigma = let lfun' = Id.Map.fold (fun id c lfun -> Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in - let sigma = Sigma.to_evar_map sigma in let ist = { ist with lfun = lfun' } in - let (sigma, c) = if is_onhyps && is_onconcl then interp_type ist (pf_env gl) sigma c else interp_constr ist (pf_env gl) sigma c - in - Sigma.Unsafe.of_pair (c, sigma) - end } in + in Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl) - end } + end end | TacChange (Some op,c,cl) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let op = interp_typed_pattern ist env sigma op in let to_catch = function Not_found -> true | e -> CErrors.is_anomaly e in - let c_interp patvars = { Sigma.run = begin fun sigma -> + let c_interp patvars sigma = let lfun' = Id.Map.fold (fun id c lfun -> Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in let ist = { ist with lfun = lfun' } in try - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = interp_constr ist env sigma c in - Sigma.Unsafe.of_pair (c, sigma) + interp_constr ist env sigma c with e when to_catch e (* Hack *) -> user_err (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") - end } in + in Tactics.change (Some op) c_interp (interp_clause ist env sigma cl) - end } + end end (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.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 - let (sigma, c) = interp_open_constr_with_bindings ist env sigma c in - Sigma.Unsafe.of_pair (c, sigma) - } in + let f env sigma = + interp_open_constr_with_bindings ist env sigma c + in (b,m,keep,f)) l in let env = Proofview.Goal.env gl in let sigma = project gl in @@ -1889,9 +1870,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.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let (sigma,c_interp) = @@ -1907,9 +1888,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 { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let hyps = interp_hyp_list ist env sigma idl in @@ -1919,20 +1900,19 @@ 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.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let (sigma,c_interp) = interp_constr ist env sigma c in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let hyps = interp_hyp_list ist env sigma idl in - let tac = name_atomic ~env + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (name_atomic ~env (TacInversion (InversionUsing (c_interp,hyps),dqhyps)) - (Leminv.lemInv_clause dqhyps c_interp hyps) - in - Sigma.Unsafe.of_pair (tac, sigma) - end } + (Leminv.lemInv_clause dqhyps c_interp hyps)) + end (* Initial call for interpretation *) @@ -1953,7 +1933,7 @@ let eval_tactic_ist ist t = let interp_tac_gen lfun avoid_ids debug t = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.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 @@ -1961,7 +1941,7 @@ let interp_tac_gen lfun avoid_ids debug t = let ltacvars = Id.Map.domain lfun in interp_tactic ist (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t) - end } + end let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t @@ -1980,9 +1960,9 @@ let hide_interp global t ot = Proofview.tclENV >>= fun env -> hide_interp env else - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> hide_interp (Proofview.Goal.env gl) - end } + end (***************************************************************************) (** Register standard arguments *) @@ -2015,37 +1995,35 @@ let () = let () = declare_uniform wit_string -let lift f = (); fun ist x -> Ftactic.enter { enter = begin fun gl -> +let lift f = (); fun ist x -> Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let sigma = Proofview.Goal.sigma gl in Ftactic.return (f ist env sigma x) -end } +end -let lifts f = (); fun ist x -> Ftactic.nf_s_enter { s_enter = begin fun gl -> +let lifts f = (); fun ist x -> Ftactic.nf_enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let sigma = Proofview.Goal.sigma gl in let (sigma, v) = f ist env sigma x in - Sigma.Unsafe.of_pair (Ftactic.return v, sigma) -end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Ftactic.return v) +end -let interp_bindings' ist bl = Ftactic.return { delayed = fun env sigma -> - let (sigma, bl) = interp_bindings ist env (Sigma.to_evar_map sigma) bl in - Sigma.Unsafe.of_pair (bl, sigma) - } +let interp_bindings' ist bl = Ftactic.return begin fun env sigma -> + interp_bindings ist env sigma bl + end -let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigma -> - let (sigma, c) = interp_constr_with_bindings ist env (Sigma.to_evar_map sigma) c in - Sigma.Unsafe.of_pair (c, sigma) - } +let interp_constr_with_bindings' ist c = Ftactic.return begin fun env sigma -> + interp_constr_with_bindings ist env sigma c + end -let interp_open_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigma -> - let (sigma, c) = interp_open_constr_with_bindings ist env (Sigma.to_evar_map sigma) c in - Sigma.Unsafe.of_pair (c, sigma) - } +let interp_open_constr_with_bindings' ist c = Ftactic.return begin fun env sigma -> + interp_open_constr_with_bindings ist env sigma c + end -let interp_destruction_arg' ist c = Ftactic.enter { enter = begin fun gl -> +let interp_destruction_arg' ist c = Ftactic.enter begin fun gl -> Ftactic.return (interp_destruction_arg ist gl c) -end } +end let interp_pre_ident ist env sigma s = s |> Id.of_string |> interp_ident ist env sigma |> Id.to_string @@ -2078,9 +2056,9 @@ let () = register_interp0 wit_ltac interp let () = - register_interp0 wit_uconstr (fun ist c -> Ftactic.enter { enter = begin fun gl -> + register_interp0 wit_uconstr (fun ist c -> Ftactic.enter begin fun gl -> Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) (Tacmach.New.project gl) c) - end }) + end) (***************************************************************************) (* Other entry points *) @@ -2111,7 +2089,7 @@ let _ = let dummy_id = Id.of_string "_" let lift_constr_tac_to_ml_tac vars tac = - let tac _ ist = Proofview.Goal.enter { enter = begin fun gl -> + let tac _ ist = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let map = function @@ -2124,7 +2102,7 @@ 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 let vernac_debug b = diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 294cba4d7..e6d0370f3 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -12,7 +12,6 @@ open Pp open Tacexpr open Termops open Nameops -open Proofview.Notations let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () @@ -57,10 +56,10 @@ let db_pr_goal gl = str" " ++ pc) ++ fnl () let db_pr_goal = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_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/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 7497aae3c..83f374346 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1668,8 +1668,6 @@ let rcst_domain_spec = lazy { dump_proof = dump_psatz coq_Q dump_q } -open Proofview.Notations - (** Naive topological sort of constr according to the subterm-ordering *) (* An element is minimal x is minimal w.r.t y if @@ -1712,7 +1710,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) (vm_of_list env) in (* todo : directly generate the proof term - or generalize before conversion? *) - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> Tacticals.New.tclTHENLIST [ Tactics.change_concl @@ -1724,7 +1722,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* ] (Tacmach.New.pf_concl gl)) ] - end } + end (** @@ -1972,7 +1970,7 @@ let micromega_gen (normalise:'cst atom -> 'cst mc_cnf) unsat deduce spec dumpexpr prover tac = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in @@ -2029,7 +2027,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) @@ -2050,7 +2048,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) (vm_of_list env) in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> Tacticals.New.tclTHENLIST [ (Tactics.change_concl @@ -2065,7 +2063,7 @@ let micromega_order_changer cert env ff = (Tacmach.New.pf_concl gl))); (* Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)*) ] - end } + end let micromega_genr prover tac = let parse_arith = parse_rarith in @@ -2080,7 +2078,7 @@ let micromega_genr prover tac = proof_typ = Lazy.force coq_QWitness ; dump_proof = dump_psatz coq_Q dump_q } in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in @@ -2144,7 +2142,7 @@ let micromega_genr prover tac = ^ "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 diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 0cd18ae50..465e77019 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -28,7 +28,6 @@ open Globnames open Nametab open Contradiction open Misctypes -open Proofview.Notations open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -38,12 +37,12 @@ open OmegaSolver (* Added by JCF, 09/03/98 *) let elim_id id = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> simplest_elim (mkVar id) - end } -let resolve_id id = Proofview.Goal.enter { enter = begin fun gl -> + end +let resolve_id id = Proofview.Goal.enter begin fun gl -> apply (mkVar id) -end } +end let timing timer_name f arg = f arg @@ -580,10 +579,10 @@ let abstract_path sigma typ path t = let focused_simpl path = let open Tacmach.New in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in convert_concl_no_check newc DEFAULTcast - end } + end let focused_simpl path = focused_simpl path @@ -643,17 +642,16 @@ let decompile af = (** Backward compat to emulate the old Refine: normalize the goal conclusion *) let new_hole env sigma c = - let c = Reductionops.nf_betaiota (Sigma.to_evar_map sigma) c in + let c = Reductionops.nf_betaiota sigma c in Evarutil.new_evar env sigma c let clever_rewrite_base_poly typ p result theorem = let open Tacmach.New in - let open Sigma in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let full = pf_concl gl in let env = pf_env gl in let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in - Refine.refine { run = begin fun sigma -> + Refine.refine begin fun sigma -> let t = applist (mkLambda @@ -667,10 +665,10 @@ let clever_rewrite_base_poly typ p result theorem = [abstracted]) in let argt = mkApp (abstracted, [|result|]) in - let Sigma (hole, sigma, p) = new_hole env sigma argt in - Sigma (applist (t, [hole]), sigma, p) - end } - end } + let (sigma, hole) = new_hole env sigma argt in + (sigma, applist (t, [hole])) + end + end let clever_rewrite_base p result theorem = clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem @@ -689,26 +687,25 @@ let clever_rewrite_gen_nat p result (t,args) = (** Solve using the term the term [t _] *) let refine_app gl t = let open Tacmach.New in - let open Sigma in - Refine.refine { run = begin fun sigma -> + Refine.refine begin fun sigma -> let env = pf_env gl in - let ht = match EConstr.kind (Sigma.to_evar_map sigma) (pf_get_type_of gl t) with + let ht = match EConstr.kind sigma (pf_get_type_of gl t) with | Prod (_, t, _) -> t | _ -> assert false in - let Sigma (hole, sigma, p) = new_hole env sigma ht in - Sigma (applist (t, [hole]), sigma, p) - end } + let (sigma, hole) = new_hole env sigma ht in + (sigma, applist (t, [hole])) + end let clever_rewrite p vpath t = let open Tacmach.New in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let full = pf_concl gl in let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in let t' = applist(t, (vargs @ [abstracted])) in refine_app gl t' - end } + end let rec shuffle p (t1,t2) = match t1,t2 with @@ -1466,7 +1463,7 @@ let reintroduce id = open Proofview.Notations let coq_omega = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> clear_constr_tables (); let hyps_types = Tacmach.New.pf_hyps_types gl in let destructure_omega = destructure_omega gl in @@ -1514,12 +1511,12 @@ let coq_omega = tclTHEN prelude (replay_history tactic_normalisation path) with NO_CONTRADICTION -> tclZEROMSG (Pp.str"Omega can't solve this system") end - end } + end let coq_omega = coq_omega let nat_inject = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in let rec explore p t : unit Proofview.tactic = Proofview.tclEVARMAP >>= fun sigma -> @@ -1655,7 +1652,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 @@ -1729,19 +1726,19 @@ let onClearedName id tac = (* so renaming may be necessary *) tclTHEN (tclTRY (clear [id])) - (Proofview.Goal.nf_enter { enter = begin fun gl -> + (Proofview.Goal.nf_enter begin fun gl -> let id = fresh_id [] id gl in tclTHEN (introduction id) (tac id) - end }) + end) let onClearedName2 id tac = tclTHEN (tclTRY (clear [id])) - (Proofview.Goal.nf_enter { enter = begin fun gl -> + (Proofview.Goal.nf_enter begin fun gl -> let id1 = fresh_id [] (add_suffix id "_left") gl in let id2 = fresh_id [] (add_suffix id "_right") gl in tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] - end }) + end) let rec is_Prop sigma c = match EConstr.kind sigma c with | Sort s -> Sorts.is_prop (ESorts.kind sigma s) @@ -1749,7 +1746,7 @@ let rec is_Prop sigma c = match EConstr.kind sigma c with | _ -> false let destructure_hyps = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in let decidability = decidability gl in let pf_nf = pf_nf gl in @@ -1888,10 +1885,10 @@ let destructure_hyps = in let hyps = Proofview.Goal.hyps gl in loop hyps - end } + end let destructure_goal = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let decidability = decidability gl in let rec loop t = @@ -1910,9 +1907,9 @@ let destructure_goal = try let dec = decidability t in tclTHEN - (Proofview.Goal.nf_enter { enter = begin fun gl -> + (Proofview.Goal.nf_enter begin fun gl -> refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |])) - end }) + end) intro with Undecidable -> Tactics.elim_type (Lazy.force coq_False) | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e @@ -1920,7 +1917,7 @@ let destructure_goal = 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 59ed8439b..ffacd8b36 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -465,12 +465,12 @@ let pf_constrs_of_globals l = in aux l [] let quote f lid = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let fg = Tacmach.New.pf_global f gl in let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in Tacticals.New.pf_constr_of_global fg >>= fun f -> pf_constrs_of_globals clg >>= fun cl -> - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let ivs = compute_ivs f (List.map (EConstr.to_constr sigma) cl) gl in @@ -483,16 +483,16 @@ 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 } + end + end let gen_quote cont c f lid = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let fg = Tacmach.New.pf_global f gl in let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in Tacticals.New.pf_constr_of_global fg >>= fun f -> pf_constrs_of_globals clg >>= fun cl -> - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let cl = List.map (EConstr.to_constr sigma) cl in @@ -505,8 +505,8 @@ 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 } + end + end (*i diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index fbed1df17..d97dea039 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -226,7 +226,7 @@ module type Int = sig val mk : Bigint.bigint -> Term.constr val parse_term : Term.constr -> parse_term - val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel + val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel (* check whether t is built only with numbers and + * - *) val get_scalar : Term.constr -> Bigint.bigint option end diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index ca23ed6c4..a452b1a91 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -113,7 +113,7 @@ module type Int = (* parsing a term (one level, except if a number is found) *) val parse_term : Term.constr -> parse_term (* parsing a relation expression, including = < <= >= > *) - val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel + val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel (* Is a particular term only made of numbers and + * - ? *) val get_scalar : Term.constr -> Bigint.bigint option end diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index fdcd62299..575634174 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -8,7 +8,6 @@ open Pp open Util -open Proofview.Notations open Const_omega module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -1029,7 +1028,7 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list = Tactics.apply (EConstr.of_constr (Lazy.force coq_I)) let total_reflexive_omega_tactic unsafe = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> Coqlib.check_required_library ["Coq";"romega";"ROmega"]; rst_omega_eq (); rst_omega_var (); @@ -1043,4 +1042,5 @@ let total_reflexive_omega_tactic unsafe = if !debug then display_systems systems_list; resolution unsafe env reified_goal systems_list with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system") - end } + end + diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index cca5cde15..85cbdc5a4 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -749,7 +749,7 @@ let ltac_ring_structure e = lemma1;lemma2;pretac;posttac] let ring_lookup (f : Value.t) lH rl t = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in try (* find_ring_strucure can raise an exception *) @@ -761,7 +761,7 @@ let ring_lookup (f : Value.t) 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 (***********************************************************************) @@ -1035,7 +1035,7 @@ let ltac_field_structure e = field_simpl_eq_in_ok;cond_ok;pretac;posttac] let field_lookup (f : Value.t) lH rl t = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in try @@ -1047,4 +1047,4 @@ let field_lookup (f : Value.t) 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 |