diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 58 |
1 files changed, 28 insertions, 30 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index b1ff0e401..3b497faab 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -497,8 +497,6 @@ let interp_fresh_id ist env sigma l = Id.of_string s in Tactics.fresh_id_in_env avoid id env - - (* Extract the uconstr list from lfun *) let extract_ltac_constr_context ist env = let open Glob_term in @@ -1785,12 +1783,12 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in - Proofview.Unsafe.tclEVARS sigma <*> - name_atomic ~env + Tacticals.New.tclWITHHOLES false + (name_atomic ~env (TacIntroPattern l) (* spiwack: print uninterpreted, not sure if it is the expected behaviour. *) - (Tactics.intros_patterns l') + (Tactics.intros_patterns l')) sigma end | TacIntroMove (ido,hto) -> Proofview.Goal.enter begin fun gl -> @@ -1824,11 +1822,11 @@ and interp_atomic ist tac : unit Proofview.tactic = (k,(loc,f))) cb in let sigma,tac = match cl with - | None -> sigma, fun l -> Tactics.apply_with_delayed_bindings_gen a ev l + | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l | Some cl -> let sigma,(clear,id,cl) = interp_in_hyp_as ist env sigma cl in - sigma, fun l -> Tactics.apply_delayed_in a ev clear id l cl in - Tacticals.New.tclWITHHOLES ev tac sigma l + sigma, Tactics.apply_delayed_in a ev clear id l cl in + Tacticals.New.tclWITHHOLES ev tac sigma end end | TacElim (ev,(keep,cb),cbo) -> @@ -1837,22 +1835,22 @@ and interp_atomic ist tac : unit Proofview.tactic = let sigma = Proofview.Goal.sigma 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 cbo = + let named_tac = let tac = Tactics.elim ev keep cb cbo in name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac in - Tacticals.New.tclWITHHOLES ev named_tac sigma cbo + Tacticals.New.tclWITHHOLES ev named_tac sigma end | TacCase (ev,(keep,cb)) -> Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in - let named_tac cb = + let named_tac = let tac = Tactics.general_case_analysis ev keep cb in name_atomic ~env (TacCase(ev,(keep,cb))) tac in - Tacticals.New.tclWITHHOLES ev named_tac sigma cb + Tacticals.New.tclWITHHOLES ev named_tac sigma end | TacFix (idopt,n) -> Proofview.Goal.enter begin fun gl -> @@ -1915,20 +1913,20 @@ and interp_atomic ist tac : unit Proofview.tactic = in let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in let tac = Option.map (interp_tactic ist) t in - Proofview.Unsafe.tclEVARS sigma <*> - name_atomic ~env + Tacticals.New.tclWITHHOLES false + (name_atomic ~env (TacAssert(b,t,ipat,c)) - (Tactics.forward b tac ipat' c) + (Tactics.forward b tac ipat' c)) sigma end | TacGeneralize cl -> Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in - Proofview.Unsafe.tclEVARS sigma <*> - name_atomic ~env + Tacticals.New.tclWITHHOLES false + (name_atomic ~env (TacGeneralize cl) - (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl)) + (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl))) sigma end | TacGeneralizeDep c -> (new_interp_constr ist c) (fun c -> @@ -1953,11 +1951,11 @@ and interp_atomic ist tac : unit Proofview.tactic = let with_eq = if b then None else Some (true,id) in Tactics.letin_tac with_eq na c None cl in - Proofview.Unsafe.tclEVARS sigma <*> let na = interp_fresh_name ist env sigma na in - name_atomic ~env + Tacticals.New.tclWITHHOLES false + (name_atomic ~env (TacLetTac(na,c_interp,clp,b,eqpat)) - (let_tac b na c_interp clp eqpat) + (let_tac b na c_interp clp eqpat)) sigma else (* We try to keep the pattern structure as much as possible *) let let_pat_tac b na c cl eqpat = @@ -1970,7 +1968,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (TacLetTac(na,c,clp,b,eqpat)) (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*) (let_pat_tac b (interp_fresh_name ist env sigma na) - ((sigma,sigma'),c) clp) sigma' eqpat) + ((sigma,sigma'),c) clp eqpat) sigma') end (* Automation tactics *) @@ -2080,11 +2078,11 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in - let named_tac bll = + let named_tac = let tac = Tactics.split_with_bindings ev bll in name_atomic ~env (TacSplit (ev, bll)) tac in - Tacticals.New.tclWITHHOLES ev named_tac sigma bll + Tacticals.New.tclWITHHOLES ev named_tac sigma end (* Conversion *) | TacReduce (r,cl) -> @@ -2184,10 +2182,10 @@ and interp_atomic ist tac : unit Proofview.tactic = in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let sigma,ids_interp = interp_or_and_intro_pattern_option ist env sigma ids in - Proofview.Unsafe.tclEVARS sigma <*> - name_atomic ~env + Tacticals.New.tclWITHHOLES false + (name_atomic ~env (TacInversion(DepInversion(k,c_interp,ids),dqhyps)) - (Inv.dinv k c_interp ids_interp dqhyps) + (Inv.dinv k c_interp ids_interp dqhyps)) sigma end | TacInversion (NonDepInversion (k,idl,ids),hyp) -> Proofview.Goal.enter begin fun gl -> @@ -2196,10 +2194,10 @@ and interp_atomic ist tac : unit Proofview.tactic = let hyps = interp_hyp_list ist env sigma idl in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let sigma, ids_interp = interp_or_and_intro_pattern_option ist env sigma ids in - Proofview.Unsafe.tclEVARS sigma <*> - name_atomic ~env + Tacticals.New.tclWITHHOLES false + (name_atomic ~env (TacInversion (NonDepInversion (k,hyps,ids),dqhyps)) - (Inv.inv_clause k ids_interp hyps dqhyps) + (Inv.inv_clause k ids_interp hyps dqhyps)) sigma end | TacInversion (InversionUsing (c,idl),hyp) -> Proofview.Goal.enter begin fun gl -> |