Commit 08df47b0 authored by charguer's avatar charguer

progress2

parent 755ada18
......@@ -2,7 +2,6 @@ Set Implicit Arguments.
(********************************************************************)
(** Treatment of partially-applied equality *)
......
......@@ -43,7 +43,7 @@ Lemma infix_emark_eq_loc_spec : curried 2%nat infix_emark_eq__ /\
forall (a b:loc),
app infix_emark_eq__ [a b] \[] \[= isTrue (a <> b) ].
Proof using.
xcf. xgo*. rew_refl; xauto*.
xcf. xgo*. rew_isTrue; xauto*.
Qed.
Lemma infix_emark_eq_gen_spec : curried 2%nat infix_emark_eq__ /\
......@@ -51,8 +51,7 @@ Lemma infix_emark_eq_gen_spec : curried 2%nat infix_emark_eq__ /\
app infix_emark_eq__ [a b] \[] (fun r => \[r = false -> isTrue (a = b)]).
Proof using.
xcf. xapp_spec infix_eq_eq_gen_spec.
introv E. xrets. introv F. fold_bool.
applys* E.
introv E. xrets~.
Qed.
Hint Extern 1 (RegisterSpec infix_emark_eq__) => Provide infix_emark_eq_loc_spec.
......
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