diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 80 |
1 files changed, 40 insertions, 40 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1ea19bce0..da3ab737b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -633,7 +633,7 @@ let pf_interp_constr ist gl = let new_interp_constr ist c k = let open Proofview in Proofview.Goal.enter { enter = begin fun gl -> - let (sigma, c) = interp_constr ist (Goal.env gl) (Goal.sigma gl) c in + let (sigma, c) = interp_constr ist (Goal.env gl) (Tacmach.New.project gl) c in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k c) end } @@ -790,11 +790,11 @@ 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.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Proofview.Goal.sigma gl) v) end + Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Tacmach.New.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.nf_enter begin fun gl -> - Ftactic.return (pr_constr_under_binders_env (pf_env gl) (Proofview.Goal.sigma gl) c) + Ftactic.return (pr_constr_under_binders_env (pf_env gl) (Tacmach.New.project gl) c) end else if has_type v (topwit wit_unit) then Ftactic.return (str "()") @@ -804,16 +804,16 @@ let rec message_of_value v = let p = out_gen (topwit wit_intro_pattern) v in let print env sigma c = pr_constr_env env sigma (fst (Tactics.run_delayed env Evd.empty c)) in Ftactic.nf_enter begin fun gl -> - Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (Proofview.Goal.sigma gl) c) p) + Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (Tacmach.New.project gl) c) p) end else if has_type v (topwit wit_constr_context) then let c = out_gen (topwit wit_constr_context) v in - Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Proofview.Goal.sigma gl) c) end + Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Tacmach.New.project gl) c) end else if has_type v (topwit wit_uconstr) then let c = out_gen (topwit wit_uconstr) v in Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_closed_glob_env (pf_env gl) - (Proofview.Goal.sigma gl) c) + (Tacmach.New.project gl) c) end else match Value.to_list v with | Some l -> @@ -1224,7 +1224,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | BindingsArgType | OptArgType _ | PairArgType _ -> (** generic handler *) Ftactic.nf_enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let goal = Proofview.Goal.goal gl in @@ -1233,7 +1233,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with end | _ as tag -> (** Special treatment. TODO: use generic handler *) Ftactic.nf_enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in match tag with | IntOrVarArgType -> @@ -1352,7 +1352,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let goal_sigma = Proofview.Goal.sigma gl in + let goal_sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in let goal = Proofview.Goal.goal gl in let tac = Tacenv.interp_ml_tactic opn in @@ -1399,7 +1399,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = match arg with | TacGeneric arg -> Ftactic.nf_enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let goal = Proofview.Goal.goal gl in let (sigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} arg in Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v) @@ -1407,7 +1407,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = | Reference r -> interp_ltac_reference dloc false ist r | ConstrMayEval c -> Ftactic.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp)) @@ -1427,12 +1427,12 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = interp_app loc ist fv largs | TacFreshId l -> Ftactic.enter begin fun gl -> - let id = interp_fresh_id ist (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) l in + let id = interp_fresh_id ist (Tacmach.New.pf_env gl) (Tacmach.New.project gl) l in Ftactic.return (in_gen (topwit wit_intro_pattern) (dloc, IntroNaming (IntroIdentifier id))) end | TacPretype c -> Ftactic.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let {closure;term} = interp_uconstr ist env c in let vars = { @@ -1611,7 +1611,7 @@ and interp_match ist lz constr lmr = end end >>= fun constr -> Ftactic.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.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) @@ -1620,7 +1620,7 @@ and interp_match ist lz constr lmr = (* Interprets the Match Context expressions *) and interp_match_goal ist lz lr lmr = Ftactic.nf_enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let hyps = Proofview.Goal.hyps gl in let hyps = if lr then List.rev hyps else hyps in @@ -1767,7 +1767,7 @@ and interp_ltac_constr ist e : constr Ftactic.t = end >>= fun result -> Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let result = Value.normalize result in try let cresult = coerce_to_closed_constr env result in @@ -1805,7 +1805,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacIntroPattern l -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in Tacticals.New.tclWITHHOLES false (name_atomic ~env @@ -1817,7 +1817,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacIntroMove (ido,hto) -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let mloc = interp_move_location ist env sigma hto in let ido = Option.map (interp_ident ist env sigma) ido in name_atomic ~env @@ -1840,7 +1840,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Trace.name_tactic (fun () -> Pp.str"<apply>") begin Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let l = List.map (fun (k,c) -> let loc, f = interp_open_constr_with_bindings_loc ist c in (k,(loc,f))) cb @@ -1856,7 +1856,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacElim (ev,(keep,cb),cbo) -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in let named_tac = @@ -1867,7 +1867,7 @@ and interp_atomic ist tac : unit Proofview.tactic = end } | TacCase (ev,(keep,cb)) -> Proofview.Goal.enter { enter = begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in let named_tac = @@ -1879,7 +1879,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacFix (idopt,n) -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let idopt = Option.map (interp_ident ist env sigma) idopt in name_atomic ~env (TacFix(idopt,n)) @@ -1905,7 +1905,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacCofix idopt -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let idopt = Option.map (interp_ident ist env sigma) idopt in name_atomic ~env (TacCofix (idopt)) @@ -1931,7 +1931,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacAssert (b,t,ipat,c) -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in @@ -1944,7 +1944,7 @@ and interp_atomic ist tac : unit Proofview.tactic = end } | TacGeneralize cl -> Proofview.Goal.enter { enter = begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.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 Tacticals.New.tclWITHHOLES false @@ -1962,7 +1962,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.V82.nf_evar_goals <*> Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let clp = interp_clause ist env sigma clp in let eqpat = interp_intro_pattern_naming_option ist env sigma eqpat in if Locusops.is_nowhere clp then @@ -2005,7 +2005,7 @@ and interp_atomic ist tac : unit Proofview.tactic = end; Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let lems = interp_auto_lemmas ist env sigma lems in name_atomic ~env (TacTrivial(debug,List.map snd lems,l)) @@ -2022,7 +2022,7 @@ and interp_atomic ist tac : unit Proofview.tactic = end; Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let lems = interp_auto_lemmas ist env sigma lems in name_atomic ~env (TacAuto(debug,n,List.map snd lems,l)) @@ -2038,7 +2038,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.V82.nf_evar_goals <*> Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let sigma,l = List.fold_map begin fun sigma (c,(ipato,ipats),cls) -> (* TODO: move sigma as a side-effect *) @@ -2071,7 +2071,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacClear (b,l) -> Proofview.Goal.enter { enter = begin fun gl -> let env = Tacmach.New.pf_env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let l = interp_hyp_list ist env sigma l in if b then name_atomic ~env (TacClear (b, l)) (Tactics.keep l) else @@ -2082,7 +2082,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacClearBody l -> Proofview.Goal.enter { enter = begin fun gl -> let env = Tacmach.New.pf_env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let l = interp_hyp_list ist env sigma l in name_atomic ~env (TacClearBody l) @@ -2097,7 +2097,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacRename l -> Proofview.Goal.enter { enter = begin fun gl -> let env = Tacmach.New.pf_env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let l = List.map (fun (id1,id2) -> interp_hyp ist env sigma id1, @@ -2112,7 +2112,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacSplit (ev,bll) -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in let named_tac = let tac = Tactics.split_with_bindings ev bll in @@ -2165,7 +2165,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.V82.nf_evar_goals <*> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in Proofview.V82.tactic begin fun gl -> let (sigma,sign,op) = interp_typed_pattern ist env sigma op in let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in @@ -2189,7 +2189,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacSymmetry c -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let cl = interp_clause ist env sigma c in name_atomic ~env (TacSymmetry cl) @@ -2207,7 +2207,7 @@ and interp_atomic ist tac : unit Proofview.tactic = } in (b,m,keep,f)) l in let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let cl = interp_clause ist env sigma cl in name_atomic ~env (TacRewrite (ev,l,cl,by)) @@ -2219,7 +2219,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacInversion (DepInversion (k,c,ids),hyp) -> Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let (sigma,c_interp) = match c with | None -> sigma , None @@ -2239,7 +2239,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacInversion (NonDepInversion (k,idl,ids),hyp) -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let hyps = interp_hyp_list ist env sigma idl in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let sigma, ids_interp = interp_or_and_intro_pattern_option ist env sigma ids in @@ -2251,7 +2251,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacInversion (InversionUsing (c,idl),hyp) -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.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 @@ -2413,7 +2413,7 @@ 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 env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let map = function | None -> None | Some id -> |