diff options
| author | Pierre-Marie Pédrot | 2017-10-30 15:53:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-10-30 17:12:16 +0100 |
| commit | a997ee7d78d90740b15b58502a1dc5e587b43ee3 (patch) | |
| tree | 0af87e2a77690deda29bec02a978076dd8f89d7e /theories | |
| parent | f18502f32fb25b29cafe26340edbbcedd463c646 (diff) | |
Introducing the change tactic.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Notations.v | 6 | ||||
| -rw-r--r-- | theories/Std.v | 2 |
2 files changed, 8 insertions, 0 deletions
diff --git a/theories/Notations.v b/theories/Notations.v index 48f3ca0587..77f3e235f3 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -375,6 +375,12 @@ Ltac2 Notation "native_compute" pl(opt(seq(pattern, occurrences))) cl(opt(clause Std.native pl (default_on_concl cl). Ltac2 Notation native_compute := native_compute. +Ltac2 change0 p cl := + let ((pat, c)) := p in + Std.change pat c (default_on_concl cl). + +Ltac2 Notation "change" c(conversion) cl(opt(clause)) := change0 c cl. + Ltac2 rewrite0 ev rw cl tac := let cl := default_on_concl cl in Std.rewrite ev rw cl tac. diff --git a/theories/Std.v b/theories/Std.v index 7831baf046..389299f266 100644 --- a/theories/Std.v +++ b/theories/Std.v @@ -175,6 +175,8 @@ Ltac2 @ external eval_pattern : (constr * occurrences) list -> constr -> constr Ltac2 @ external eval_vm : (pattern * occurrences) option -> constr -> constr := "ltac2" "eval_vm". Ltac2 @ external eval_native : (pattern * occurrences) option -> constr -> constr := "ltac2" "eval_native". +Ltac2 @ external change : pattern option -> (constr array -> constr) -> clause -> unit := "ltac2" "tac_change". + Ltac2 @ external rewrite : evar_flag -> rewriting list -> clause -> (unit -> unit) option -> unit := "ltac2" "tac_rewrite". Ltac2 @ external reflexivity : unit -> unit := "ltac2" "tac_reflexivity". |