Commit bfd56995 authored by Michael Sammler's avatar Michael Sammler
Browse files

no trivial in done_no_false

parent 9da8555a
Pipeline #57404 passed with stage
in 12 minutes and 21 seconds
...@@ -68,12 +68,12 @@ Ltac done_no_false := ...@@ -68,12 +68,12 @@ Ltac done_no_false :=
solve solve
[ repeat first [ repeat first
[ fast_done [ fast_done
| solve [trivial] (* | solve [trivial] *)
(* All the tactics below will introduce themselves anyway, or make no sense (* All the tactics below will introduce themselves anyway, or make no sense
for goals of product type. So this is a good place for us to do it. *) for goals of product type. So this is a good place for us to do it. *)
| progress intros | progress intros
| solve [symmetry; trivial] (* | solve [symmetry; trivial] *)
| solve [apply not_symmetry; trivial] (* | solve [apply not_symmetry; trivial] *)
| split ] | split ]
]. ].
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment