diff options
| author | Maxime Dénès | 2017-05-09 22:14:35 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-06 12:58:57 +0200 |
| commit | 954fbd3b102060ed1e2122f571a430f05a174e42 (patch) | |
| tree | a6f3db424624eae05ded3be6a84357d1ad291eda /plugins | |
| parent | 2f23c27e08f66402b8fba4745681becd402f4c5c (diff) | |
Remove the Sigma (monotonous state) API.
Reminder of (some of) the reasons for removal:
- Despite the claim in sigma.mli, it does *not* prevent evar
leaks, something like:
fun env evd ->
let (evd',ev) = new_evar env evd in
(evd,ev)
will typecheck even with Sigma-like type annotations (with a proof of
reflexivity)
- The API stayed embryonic. Even typing functions were not ported to
Sigma.
- Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly
less unsafe ones (e.g. s_enter), but those ones were not marked unsafe
at all (despite still being so).
- There was no good story for higher order functions manipulating evar
maps. Without higher order, one can most of the time get away with
reusing the same name for the updated evar map.
- Most of the code doing complex things with evar maps was using unsafe
casts to sigma. This code should be fixed, but this is an orthogonal
issue.
Of course, this was showing a nice and elegant use of GADTs, but the
cost/benefit ratio in practice did not seem good.
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 33a9dd4fd9..6281b2675e 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 43c06a54d4..b638f23606 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 bbb9feae2e..e3fab6d012 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 ab1dd07c11..0fa3089e73 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 04bca584f3..e1d765a420 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 f745dbeb4b..b7fe25a32a 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 a6290cb00c..317444cf16 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 c2f705898f..fd49623986 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 a0eb9e2b27..b8070ff885 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 bd2ac8c67b..d28e0aba0a 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 a23c51495c..f1a9758e80 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 e6f199dbae..ff397d2e92 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 0a13a20a97..ea1660d901 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 bf84f61a5b..7db484d825 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 9726a5b401..8afe3053d0 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 50e8255a67..2c2a4b8509 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 23ce368eea..dd5307638c 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 5adf8475ae..25258ffa90 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 9029858279..9446f9df4d 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 f028abde9a..68dc1fd376 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 b78dc37426..cfb698cd87 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 37fdd185e9..ff76d06cf3 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 294cba4d75..e6d0370f36 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 7497aae3ca..83f374346e 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 0cd18ae506..465e770199 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 59ed8439b6..ffacd8b361 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 fbed1df176..d97dea0397 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 ca23ed6c42..a452b1a917 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 fdcd622994..575634174f 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 cca5cde155..85cbdc5a41 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 |