Commit 7695877b authored by Michael Sammler's avatar Michael Sammler
Browse files

remove via_vm_compute

parent a48c304d
Pipeline #55396 passed with stage
in 30 minutes and 4 seconds
......@@ -47,19 +47,3 @@ Class CanSolve (P : Prop) : Prop := can_solve: P.
Definition shelve_hint (P : Prop) : Prop := P.
Typeclasses Opaque shelve_hint.
Arguments shelve_hint : simpl never.
(** * [via_vm_compute]
[via_vm_compute f a] is equivalent to [f a] but tells the automation that it should
be reduced using [vm_compute]
*)
Definition via_vm_compute_def {A B} (f : A B) (x : A) : B :=
f x.
Definition via_vm_compute_aux : seal (@via_vm_compute_def). by eexists. Qed.
Definition via_vm_compute := unseal via_vm_compute_aux.
Definition via_vm_compute_eq' : @via_vm_compute = @via_vm_compute_def :=
seal_eq via_vm_compute_aux.
Arguments via_vm_compute {_ _} _ _.
Lemma via_vm_compute_eq {A B} (f : A B) x:
via_vm_compute f x = f x.
Proof. rewrite via_vm_compute_eq'. done. Qed.
......@@ -704,15 +704,6 @@ Ltac liSideCond :=
lazymatch P with
| shelve_hint _ => split; [ unfold shelve_hint; li_shelve_sidecond |]
| _ => first [
match P with
| context C [via_vm_compute ?f ?a] =>
rewrite (via_vm_compute_eq f a);
(* TODO: using [vm_compute (f a)] leads to very slow QED. Why is this the case? *)
(* vm_compute (f a) *)
let x := eval vm_compute in (f a) in
let P' := context C [ x ] in
change_no_check (P' Q)
end |
progress normalize_goal_and |
lazymatch P with
| context [protected _] => first [
......
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