Skip to content

I
Iris
Commit ed90ff31 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Comment on commit 44cfd7d3.

parent 44cfd7d3
Pipeline #3033 passed with stage
    in 10 minutes and 12 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 1 addition and 0 deletions
    prelude/tactics.v
    View file @ ed90ff31
    ......@@ -479,6 +479,7 @@ Tactic Notation "naive_solver" tactic(tac) :=
    (**i simplification of assumptions *)
    | H : False |- _ => destruct H
    | H : _ ∧ _ |- _ =>
    (* Work around bug https://coq.inria.fr/bugs/show_bug.cgi?id=2901 *)
    let H1 := fresh in let H2 := fresh in
    destruct H as [H1 H2]; try clear H
    | H : ∃ _, _ |- _ =>
    ......
    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