diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-26 16:54:56 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-26 16:54:56 +0200 |
| commit | 39b4d1d31c6446c937164039cac585dbe91b8b29 (patch) | |
| tree | 9de2490006271f4e0bc348b469d788d971c1ebc3 /src | |
| parent | 1cd1e8d4e3399a582c2f5b8de203ba59cd3f8010 (diff) | |
| download | smtcoq-39b4d1d31c6446c937164039cac585dbe91b8b29.tar.gz smtcoq-39b4d1d31c6446c937164039cac585dbe91b8b29.zip | |
CompDec are automatically discharged when generated by the OCaml tactic, when possible
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) ]. |