Commit 7a1421d1 authored by Ralf Jung's avatar Ralf Jung
Browse files

preserve mk_evar support for type coercions (by Robbert)

parent 394c8d20
Pipeline #50633 passed with stage
in 5 minutes and 8 seconds
......@@ -60,6 +60,20 @@ Lemma naive_solver_issue_115 (P : nat → Prop) (x : nat) :
( x', P x' x' = 10) P x x + 1 = 11.
Proof. naive_solver. Qed.
(** [mk_evar] works on things that coerce to types. *)
(** This is a feature when we have packed structures, for example Iris's [ofe]
(fields other than the carrier omitted). *)
Structure ofe := Ofe { ofe_car :> Type }.
Goal A : ofe, True.
intros A.
let x := mk_evar A in idtac.
Abort.
(** More surprisingly, it also works for other coercions into a
universe, like [Is_true : bool → Prop]. *)
Goal True.
let x := mk_evar true in idtac.
Abort.
(** Make sure that [done] is not called recursively when solving [is_Some],
which might leave an unresolved evar before performing ex falso. *)
Goal False is_Some (@None nat).
......
......@@ -231,6 +231,7 @@ trick described at
<https://stackoverflow.com/questions/45949064/check-for-evars-in-a-tactic-that-returns-a-value/46178884#46178884>
to work around that: wrap the side-effect in a [match goal]. *)
Ltac mk_evar T :=
let T := constr:(T : Type) in
let e := fresh in
let _ := match goal with _ => evar (e:T) end in
let e' := eval unfold e in e in
......
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