Commit 926a3657 authored by Dan Frumin's avatar Dan Frumin

Fix a bug/typo in reshape_expr

parent 99da4c96
......@@ -51,7 +51,7 @@ Ltac reshape_expr e tac :=
| Unfold ?e => go (UnfoldCtx :: K) e
| TApp ?e => go (TAppCtx :: K) e
| Pack ?e => go (PackCtx :: K) e
| Unpack ?e1 ?e2 => go (UnpackLCtx e2 :: K) e
| Unpack ?e1 ?e2 => go (UnpackLCtx e2 :: K) e1
| Alloc ?e => go (AllocCtx :: K) e
| Load ?e => go (LoadCtx :: K) e
| Store ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (StoreRCtx v1 :: K) e2)
......@@ -122,8 +122,7 @@ Tactic Notation "tp_normalise" constr(j) :=
| lazymatch goal with
| |- fill ?K ?e = _ =>
by rewrite /= ?fill_app /=
| |- ?e = _ =>
idtac "nice"
(* | |- ?e = _ => rewrite /= ?fill_nil /= *)
end
|env_cbv; reflexivity
|(* new goal *)].
......
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