diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-26 17:01:07 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-26 17:01:07 +0200 |
commit | 5cb4fb6fbda54976254255ffa5a428f63dee6115 (patch) | |
tree | 39a548f866d5cf3fbbc750f1b79b2be06baf37f2 /src | |
parent | d90e8b221455dafa32db03f9fdb1601f3127474f (diff) | |
parent | 3c16cd6919f2f44cf2732e0bcda88b91ddbbbcff (diff) | |
download | smtcoq-5cb4fb6fbda54976254255ffa5a428f63dee6115.tar.gz smtcoq-5cb4fb6fbda54976254255ffa5a428f63dee6115.zip |
Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11
Diffstat (limited to 'src')
-rw-r--r-- | src/versions/standard/Tactics_standard.v | 31 |
1 files changed, 17 insertions, 14 deletions
diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v index 468de7a..232ae54 100644 --- a/src/versions/standard/Tactics_standard.v +++ b/src/versions/standard/Tactics_standard.v @@ -66,25 +66,28 @@ End Test. (** Tactics in bool *) +Tactic Notation "verit_bool_base_auto" constr(h) := verit_bool_base h; auto with typeclass_instances. +Tactic Notation "verit_bool_no_check_base_auto" constr(h) := verit_bool_no_check_base h; auto with typeclass_instances. + Tactic Notation "verit_bool" constr(h) := get_hyps ltac:(fun Hs => match Hs with - | Some ?Hs => verit_bool_base (Some (h, Hs)) - | None => verit_bool_base (Some h) + | Some ?Hs => verit_bool_base_auto (Some (h, Hs)) + | None => verit_bool_base_auto (Some h) end; vauto). Tactic Notation "verit_bool" := - get_hyps ltac:(fun Hs => verit_bool_base Hs; vauto). + get_hyps ltac:(fun Hs => verit_bool_base_auto Hs; vauto). Tactic Notation "verit_bool_no_check" constr(h) := get_hyps ltac:(fun Hs => match Hs with - | Some ?Hs => verit_bool_no_check_base (Some (h, Hs)) - | None => verit_bool_no_check_base (Some h) + | Some ?Hs => verit_bool_no_check_base_auto (Some (h, Hs)) + | None => verit_bool_no_check_base_auto (Some h) end; vauto). Tactic Notation "verit_bool_no_check" := - get_hyps ltac:(fun Hs => verit_bool_no_check_base Hs; vauto). + get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto Hs; vauto). (** Tactics in Prop **) @@ -99,8 +102,8 @@ Tactic Notation "verit" constr(h) := match Hs with | Some ?Hs => prop2bool_hyps Hs; - [ .. | verit_bool_base (Some (h, Hs)) ] - | None => verit_bool_base (Some h) + [ .. | verit_bool_base_auto (Some (h, Hs)) ] + | None => verit_bool_base_auto (Some h) end; vauto) ] ]. @@ -110,8 +113,8 @@ Tactic Notation "verit" := match Hs with | Some ?Hs => prop2bool_hyps Hs; - [ .. | verit_bool_base (Some Hs) ] - | None => verit_bool_base (@None nat) + [ .. | verit_bool_base_auto (Some Hs) ] + | None => verit_bool_base_auto (@None nat) end; vauto) ]. Tactic Notation "verit_no_check" constr(h) := @@ -121,8 +124,8 @@ Tactic Notation "verit_no_check" constr(h) := match Hs with | Some ?Hs => prop2bool_hyps Hs; - [ .. | verit_bool_no_check_base (Some (h, Hs)) ] - | None => verit_bool_no_check_base (Some h) + [ .. | verit_bool_no_check_base_auto (Some (h, Hs)) ] + | None => verit_bool_no_check_base_auto (Some h) end; vauto) ] ]. @@ -132,8 +135,8 @@ Tactic Notation "verit_no_check" := match Hs with | Some ?Hs => prop2bool_hyps Hs; - [ .. | verit_bool_no_check_base (Some Hs) ] - | None => verit_bool_no_check_base (@None nat) + [ .. | verit_bool_no_check_base_auto (Some Hs) ] + | None => verit_bool_no_check_base_auto (@None nat) end; vauto) ]. |