diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/coretactics.ml4 | 31 | ||||
| -rw-r--r-- | ltac/extraargs.ml4 | 19 | ||||
| -rw-r--r-- | ltac/extraargs.mli | 7 | ||||
| -rw-r--r-- | ltac/tacintern.ml | 14 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 42 | ||||
| -rw-r--r-- | ltac/tacinterp.mli | 3 | ||||
| -rw-r--r-- | ltac/tacsubst.ml | 6 |
7 files changed, 59 insertions, 63 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index ce28eacc09..9879cfc280 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -26,6 +26,10 @@ TACTIC EXTEND reflexivity [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] END +TACTIC EXTEND exact + [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ] +END + TACTIC EXTEND assumption [ "assumption" ] -> [ Tactics.assumption ] END @@ -197,6 +201,19 @@ TACTIC EXTEND intros_until [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ] END +TACTIC EXTEND intro +| [ "intro" ] -> [ Tactics.intro_move None MoveLast ] +| [ "intro" ident(id) ] -> [ Tactics.intro_move (Some id) MoveLast ] +| [ "intro" ident(id) "at" "top" ] -> [ Tactics.intro_move (Some id) MoveFirst ] +| [ "intro" ident(id) "at" "bottom" ] -> [ Tactics.intro_move (Some id) MoveLast ] +| [ "intro" ident(id) "after" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveAfter h) ] +| [ "intro" ident(id) "before" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveBefore h) ] +| [ "intro" "at" "top" ] -> [ Tactics.intro_move None MoveFirst ] +| [ "intro" "at" "bottom" ] -> [ Tactics.intro_move None MoveLast ] +| [ "intro" "after" hyp(h) ] -> [ Tactics.intro_move None (MoveAfter h) ] +| [ "intro" "before" hyp(h) ] -> [ Tactics.intro_move None (MoveBefore h) ] +END + (** Move *) TACTIC EXTEND move @@ -206,6 +223,12 @@ TACTIC EXTEND move | [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ] END +(** Rename *) + +TACTIC EXTEND rename +| [ "rename" ne_rename_list_sep(ids, ",") ] -> [ Tactics.rename_hyp ids ] +END + (** Revert *) TACTIC EXTEND revert @@ -222,6 +245,13 @@ TACTIC EXTEND simple_destruct [ "simple" "destruct" quantified_hypothesis(h) ] -> [ Tactics.simple_destruct h ] END +(** Double induction *) + +TACTIC EXTEND double_induction + [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] -> + [ Elim.h_double_induction h1 h2 ] +END + (* Admit *) TACTIC EXTEND admit @@ -280,7 +310,6 @@ let initial_atomic () = "hnf", TacReduce(Hnf,nocl); "simpl", TacReduce(Simpl (Redops.all_flags,None),nocl); "compute", TacReduce(Cbv Redops.all_flags,nocl); - "intro", TacIntroMove(None,MoveLast); "intros", TacIntroPattern []; ] in diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index 0bddcc9fdd..e6d0a9c69c 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -15,6 +15,7 @@ open Constrarg open Pcoq.Prim open Pcoq.Constr open Names +open Tacmach open Tacexpr open Taccoerce open Tacinterp @@ -175,6 +176,16 @@ ARGUMENT EXTEND lglob [ lconstr(c) ] -> [ c ] END +let interp_casted_constr ist gl c = + interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c + +ARGUMENT EXTEND casted_constr + TYPED AS constr + PRINTED BY pr_gen + INTERPRETED BY interp_casted_constr + [ constr(c) ] -> [ c ] +END + type 'id gen_place= ('id * hyp_location_flag,unit) location type loc_place = Id.t Loc.located gen_place @@ -225,6 +236,14 @@ ARGUMENT EXTEND hloc END +let pr_rename _ _ _ (n, m) = Nameops.pr_id n ++ str " into " ++ Nameops.pr_id m + +ARGUMENT EXTEND rename + TYPED AS ident * ident + PRINTED BY pr_rename +| [ ident(n) "into" ident(m) ] -> [ (n, m) ] +END + (* Julien: Mise en commun des differentes version de replace with in by *) let pr_by_arg_tac _prc _prlc prtac opt_c = diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli index 4d1d8ba7fe..0cf77935c2 100644 --- a/ltac/extraargs.mli +++ b/ltac/extraargs.mli @@ -16,6 +16,8 @@ val wit_orient : bool Genarg.uniform_genarg_type val orient : bool Pcoq.Gram.entry val pr_orient : bool -> Pp.std_ppcmds +val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type + val occurrences : (int list or_var) Pcoq.Gram.entry val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type val pr_occurrences : int list or_var -> Pp.std_ppcmds @@ -38,6 +40,11 @@ val wit_lconstr : Tacexpr.glob_constr_and_expr, Constr.t) Genarg.genarg_type +val wit_casted_constr : + (constr_expr, + Tacexpr.glob_constr_and_expr, + Constr.t) Genarg.genarg_type + val glob : constr_expr Pcoq.Gram.entry val lglob : constr_expr Pcoq.Gram.entry diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index 3744449e97..d39f835528 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -481,10 +481,6 @@ let rec intern_atomic lf ist x = (* Basic tactics *) | TacIntroPattern l -> TacIntroPattern (List.map (intern_intro_pattern lf ist) l) - | TacIntroMove (ido,hto) -> - TacIntroMove (Option.map (intern_ident lf ist) ido, - intern_move_location ist hto) - | TacExact c -> TacExact (intern_constr ist c) | TacApply (a,ev,cb,inhyp) -> TacApply (a,ev,List.map (intern_constr_with_bindings_arg ist) cb, Option.map (intern_in_hyp_as ist lf) inhyp) @@ -520,16 +516,6 @@ let rec intern_atomic lf ist x = Option.map (intern_or_and_intro_pattern_loc lf ist) ipats), Option.map (clause_app (intern_hyp_location ist)) cls)) l, Option.map (intern_constr_with_bindings ist) el)) - | TacDoubleInduction (h1,h2) -> - let h1 = intern_quantified_hypothesis ist h1 in - let h2 = intern_quantified_hypothesis ist h2 in - TacDoubleInduction (h1,h2) - (* Context management *) - | TacRename l -> - TacRename (List.map (fun (id1,id2) -> - intern_hyp ist id1, - intern_hyp ist id2) l) - (* Conversion *) | TacReduce (r,cl) -> dump_glob_red_expr r; diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index fcc29a8302..5ee9b0fc4d 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -684,10 +684,6 @@ let interp_typed_pattern ist env sigma (_,c,_) = interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in pattern_of_constr env sigma c -(* Interprets a constr expression casted by the current goal *) -let pf_interp_casted_constr ist gl c = - interp_constr_gen (OfType (pf_concl gl)) ist (pf_env gl) (project gl) c - (* Interprets a constr expression *) let pf_interp_constr ist gl = interp_constr ist (pf_env gl) (project gl) @@ -1644,24 +1640,6 @@ and interp_atomic ist tac : unit Proofview.tactic = expected behaviour. *) (Tactics.intro_patterns l')) sigma end } - | TacIntroMove (ido,hto) -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = 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 - (TacIntroMove(ido,mloc)) - (Tactics.intro_move ido mloc) - end } - | TacExact c -> - (* spiwack: until the tactic is in the monad *) - Proofview.Trace.name_tactic (fun () -> Pp.str"<exact>") begin - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> - let (sigma, c_interp) = pf_interp_casted_constr ist gl c in - Sigma.Unsafe.of_pair (Tactics.exact_no_check c_interp, 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 @@ -1822,26 +1800,6 @@ and interp_atomic ist tac : unit Proofview.tactic = in Sigma.Unsafe.of_pair (tac, sigma) end } - | TacDoubleInduction (h1,h2) -> - let h1 = interp_quantified_hypothesis ist h1 in - let h2 = interp_quantified_hypothesis ist h2 in - name_atomic - (TacDoubleInduction (h1,h2)) - (Elim.h_double_induction h1 h2) - (* Context management *) - | TacRename l -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = pf_env gl in - let sigma = project gl in - let l = - List.map (fun (id1,id2) -> - interp_hyp ist env sigma id1, - interp_ident ist env sigma (snd id2)) l - in - name_atomic ~env - (TacRename l) - (Tactics.rename_hyp l) - end } (* Conversion *) | TacReduce (r,cl) -> diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli index 8bb6ee4cdf..6f64981eff 100644 --- a/ltac/tacinterp.mli +++ b/ltac/tacinterp.mli @@ -72,6 +72,9 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map -> Id.t Loc.located -> Id.t +val interp_constr_gen : Pretyping.typing_constraint -> interp_sign -> + Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr + val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr bindings -> Evd.evar_map * constr bindings diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 3f504b7f37..2c3c76ef74 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -137,8 +137,6 @@ let rec subst_match_goal_hyps subst = function let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Basic tactics *) | TacIntroPattern l -> TacIntroPattern (List.map (subst_intro_pattern subst) l) - | TacIntroMove _ as x -> x - | TacExact c -> TacExact (subst_glob_constr subst c) | TacApply (a,ev,cb,cl) -> TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl) | TacElim (ev,cb,cbo) -> @@ -162,10 +160,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with subst_induction_arg subst c, ids, cls) l in let el' = Option.map (subst_glob_with_bindings subst) el in TacInductionDestruct (isrec,ev,(l',el')) - | TacDoubleInduction (h1,h2) as x -> x - - (* Context management *) - | TacRename l as x -> x (* Conversion *) | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl) |