diff options
| author | Pierre-Marie Pédrot | 2017-09-14 00:15:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-14 00:36:18 +0200 |
| commit | c53fb4be8c65a89dd03d4aedc2fc65d9807da915 (patch) | |
| tree | 62c830e3c4262ba306dee2dda7ef1141fd45be41 /theories | |
| parent | 4ed40a9427f67ab6091f1af5457ffdec5e156d12 (diff) | |
Binding the pose/set family of tactics.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Notations.v | 27 | ||||
| -rw-r--r-- | theories/Std.v | 2 |
2 files changed, 22 insertions, 7 deletions
diff --git a/theories/Notations.v b/theories/Notations.v index 9b2b04f9e6..65b05113ae 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -270,6 +270,27 @@ Ltac2 Notation "apply" cl(opt(seq(keyword("in"), ident, opt(seq(keyword("as"), intropattern))))) := apply0 true false cb cl. +Ltac2 default_on_concl cl := +match cl with +| None => { Std.on_hyps := Some []; Std.on_concl := Std.AllOccurrences } +| Some cl => cl +end. + +Ltac2 pose0 ev p := + enter_h ev (fun ev ((na, p)) => Std.pose na p) p. + +Ltac2 Notation "pose" p(thunk(pose)) := + pose0 false p. + +Ltac2 Notation "epose" p(thunk(pose)) := + pose0 true p. + +Ltac2 Notation "set" p(thunk(pose)) cl(opt(clause)) := + Std.set false p (default_on_concl cl). + +Ltac2 Notation "eset" p(thunk(pose)) cl(opt(clause)) := + Std.set true p (default_on_concl cl). + Ltac2 induction0 ev ic use := let f ev use := Std.induction ev ic use in enter_h ev f use. @@ -323,12 +344,6 @@ Ltac2 Notation "inversion_clear" ids(opt(seq("in", list1(ident)))) := Std.inversion Std.FullInversionClear arg pat ids. -Ltac2 default_on_concl cl := -match cl with -| None => { Std.on_hyps := Some []; Std.on_concl := Std.AllOccurrences } -| Some cl => cl -end. - Ltac2 Notation "red" cl(opt(clause)) := Std.red (default_on_concl cl). Ltac2 Notation red := red. diff --git a/theories/Std.v b/theories/Std.v index f8b269dce6..42bd9edde0 100644 --- a/theories/Std.v +++ b/theories/Std.v @@ -135,7 +135,7 @@ Ltac2 @ external assert : constr -> (unit -> unit) option option -> intro_patter Ltac2 @ external enough : constr -> (unit -> unit) option option -> intro_pattern option -> unit := "ltac2" "tac_enough". Ltac2 @ external pose : ident option -> constr -> unit := "ltac2" "tac_pose". -Ltac2 @ external set : evar_flag -> ident option -> (unit -> constr) -> clause -> unit := "ltac2" "tac_set". +Ltac2 @ external set : evar_flag -> (unit -> ident option * constr) -> clause -> unit := "ltac2" "tac_set". Ltac2 @ external destruct : evar_flag -> induction_clause list -> constr_with_bindings option -> unit := "ltac2" "tac_induction". |