Commit 53a108a6 authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers
Browse files

Apply 1 suggestion(s) to 1 file(s)

parent 967cda05
Pipeline #50451 passed with stage
in 4 minutes and 39 seconds
......@@ -40,6 +40,7 @@ Proof. congruence. Qed.
Definition is_Some {A} (mx : option A) := x, mx = Some x.
Global Instance: Params (@is_Some) 1 := {}.
(** We avoid calling [done] recursively as that can lead to an unresolved evar. *)
Global Hint Extern 0 (is_Some _) => eexists; fast_done : core.
Lemma is_Some_alt {A} (mx : option A) :
......
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