Skip to content

GitLab

C
cfml
Commit 5f5094da authored by Armaël Guéneau's avatar Armaël Guéneau
Browse files
Options

Fix xspec for record operations in presence of several records

parent 410635e3
Show whitespace changes
Inline Side-by-side
Showing with 4 additions and 4 deletions
lib/coq/CFTactics.v
View file @ 5f5094da
...@@ -2895,17 +2895,17 @@ Ltac xspec_record_set_compute_for f w L := ...@@ -2895,17 +2895,17 @@ Ltac xspec_record_set_compute_for f w L :=
[ reflexivity | revert G ]. [ reflexivity | revert G ].
(* extract the record contents *) (* extract the record contents *)
Ltac xspec_record_repr_compute H := Ltac xspec_record_repr_compute H r :=
match H with context [ ?r ~> record_repr ?L ] => constr:(L) end. match H with context [ r ~> record_repr ?L ] => constr:(L) end.
Ltac xspec_record_get_compute tt := Ltac xspec_record_get_compute tt :=
match goal with |- app record_get [?r ?f] ?H _ => match goal with |- app record_get [?r ?f] ?H _ =>
let L := xspec_record_repr_compute H in let L := xspec_record_repr_compute H r in
xspec_record_get_compute_for f L end. xspec_record_get_compute_for f L end.
Ltac xspec_record_set_compute tt := Ltac xspec_record_set_compute tt :=
match goal with |- app record_set [?r ?f ?w] ?H _ => match goal with |- app record_set [?r ?f ?w] ?H _ =>
let L := xspec_record_repr_compute H in let L := xspec_record_repr_compute H r in
xspec_record_set_compute_for f w L end. xspec_record_set_compute_for f w L end.
......
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