Commit 0e0fd751 authored by charguer's avatar charguer

new xclose

parent 79ba7394
......@@ -2,7 +2,7 @@ Set Implicit Arguments.
Require Import CFML.CFLib.
Require Import Demo_ml.
Require Import Stdlib.
Require LibListZ.
Require TLC.LibListZ.
Import ZsubNoSimpl.
Open Scope tag_scope.
......@@ -1427,7 +1427,16 @@ Proof using.
xcf. dup 2.
{ xopen r. xpull ;=> n E. skip. }
{ xopenx r ;=> n E. xapps. xapps. xapps. xapp.
xclose r. rew_list; math. xsimpl~. }
intros v.
dup 4.
{ (* details *)
xclose_show_core r. xchange H. skip. skip. (* demo *) }
{ (* with explicit arguments, incorrect instantiation *)
xclose (>> r L n). auto. skip. skip. (* demo *) }
{ (* with explicit arguments, correct instantiation *)
xclose (>> r (x::L) (n+1)). rew_list; math. xsimpl~. }
{ (* short form *)
xclose r. rew_list; math. xsimpl~. } }
Qed.
......
......@@ -968,22 +968,33 @@ Tactic Notation "xopenxs" constr(t) :=
*)
Ltac xclose_constr t :=
Ltac xclose_get_ptr args :=
match args with (boxer ?t)::_ => t end.
Ltac xclose_constr args :=
let t := xclose_get_ptr args in
match get_refocus_args tt with (?H1,?H2) =>
get_refocus_constr_in H1 t end.
Ltac xclose_core t :=
let C1 := xclose_constr t in
Ltac xclose_core args :=
let args := list_boxer_of args in
let C1 := xclose_constr args in
ltac_database_get database_xclose C1;
let K := fresh "TEMP" in
intros K; xchange (K t); clear K.
intros K;
let E := constr:((boxer K)::args) in
xchange E;
clear K.
Ltac xclose_show_core t :=
let C1 := xclose_constr t in
Ltac xclose_show_core args :=
let args := list_boxer_of args in
let C1 := xclose_constr args in
pose C1;
try ltac_database_get database_xclose C1;
intros.
Tactic Notation "xclose_show" constr(t) :=
xclose_show_core t.
......
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