Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Adapt to https://github.com/coq/coq/pull/19530 #8

Merged
merged 1 commit into from
Sep 18, 2024
Merged

Adapt to https://github.com/coq/coq/pull/19530 #8

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion coq/PerformanceDemos/constr_eq.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
(** * Performance Criterion: fast alpha-equivalence check (Õ(term size)) *)
Require Import Coq.ZArith.ZArith.
From Coq Require Import ZArith.

Fixpoint biga (n : nat) (f : Prop -> Prop)
:= match n with
Expand Down
2 changes: 1 addition & 1 deletion coq/PerformanceDemos/lift_identity_evar_subst.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
(** * Performance Criterion: lifting identity evar substitution should Õ(1) *)
Require Import Coq.Lists.List.
From Coq Require Import List.
(** For this test, we construct [x] evars each with context size [y]
and then we β-reduce to move them under a context with an
additional [z] elements. We also check to see how long it takes
Expand Down
2 changes: 1 addition & 1 deletion coq/PerformanceDemos/lift_non_identity_evar_subst.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
(** * Performance Criterion: lifting identity evar substitution should Õ(1) *)
Require Import Coq.Lists.List.
From Coq Require Import List.
(** For this test, we construct [x] evars each with context size [y],
then we β-reduce to make the substitution non-identity. Then we
β-reduce again to move them under a context with an additional [z]
Expand Down
2 changes: 1 addition & 1 deletion coq/PerformanceDemos/quadratic_reduction.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
(* -*- coq-prog-args: ("-debug") -*- *)
(** * Full reduction on a function of complexity O(f) should be Õ(f + input term size + output term size) *)
Require Import Coq.Lists.List.
From Coq Require Import List.
(** Copied from COQBUG(https://github.com/coq/coq/issues/11964) *)
Module Red.
Inductive type := NAT | LIST (t : type) | ARROW (A B : type).
Expand Down
4 changes: 2 additions & 2 deletions coq/PerformanceDemos/rewrite_strat_repeated_app.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
(** * performance of turning f (f (... (f x))) = g (g (... (g x))) given f x = g x (or x = y -> f x = g y) w/ rewrite_strat *)
Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
From Coq Require Import Setoid Morphisms.
Axiom f : nat -> nat.
Axiom g : nat -> nat.
Axiom fg : forall x, f x = g x.
Expand Down Expand Up @@ -109,7 +109,7 @@ Evars: 2012 -> 0
Finished transaction in 8.697 secs (8.693u,0.004s) (successful)
Finished transaction in 0.185 secs (0.185u,0.s) (successful) *)

Require Import Coq.ssr.ssreflect.
From Coq Require Import ssreflect.
Goal forall x, (f^100) x = (g^100) x. cbv [comp_pow]; intro. Time rewrite !fg. reflexivity. Abort.
(* Finished transaction in 0.114 secs (0.114u,0.s) (successful) *)
Goal forall x, (f^200) x = (g^200) x. cbv [comp_pow]; intro. Time rewrite !fg. reflexivity. Abort.
Expand Down
4 changes: 2 additions & 2 deletions coq/PerformanceDemos/rewrite_strat_under_binders.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
(** * performance of rewrite/rewrite_strat under binders *)
Require Import Coq.Classes.Morphisms.
Require Import Coq.Setoids.Setoid.
From Coq Require Import Morphisms.
From Coq Require Import Setoid.
Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y.
Strategy 100 [Let_In].
Global Hint Opaque Let_In : rewrite.
Expand Down
2 changes: 1 addition & 1 deletion coq/PerformanceExperiments/.coq-version
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
Welcome to Coq 8.11.1 (April 2020) The Coq Proof Assistant, version 8.11.1 (April 2020) compiled on Apr 4 2020 17:41:20 with OCaml 4.06.1
Welcome to Coq WDTIS2222H:/home/pgroux/git/coq/_build/default,split_stdlib (e21cd4a2217dc094ab774e3209ae29ea6223eca7) The Coq Proof Assistant, version 8.21+alpha compiled with OCaml 4.14.1
12 changes: 6 additions & 6 deletions coq/PerformanceExperiments/Harness.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
Require Import Coq.Structures.Orders.
Require Import Coq.micromega.Lia.
Require Import Coq.Bool.Bool.
Require Import Coq.Sorting.Mergesort.
Require Export Coq.Lists.List.
Require Export Coq.ZArith.ZArith.
From Coq Require Import Orders.
From Coq Require Import Lia.
From Coq Require Import Bool.
From Coq Require Import Mergesort.
From Coq Require Export List.
From Coq Require Export ZArith.
Export ListNotations.

Global Set Printing Width 1000.
Expand Down
8 changes: 4 additions & 4 deletions coq/PerformanceExperiments/conj_True_fast_conj/_0_Sanity.log
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,13 @@ Tactic call abstract-fast_conj ran for 0. secs (0.u,0.s) (success)
Tactic call close-abstract ran for 0. secs (0.u,0.s)
Params: n= 2
Tactic call refine ran for 0. secs (0.u,0.s) (success)
Tactic call pose build and refine ran for 0. secs (0.u,0.s) (success)
Tactic call fast_conj ran for 0. secs (0.u,0.s) (success)
Tactic call abstract-fast_conj ran for 0. secs (0.u,0.s) (success)
Tactic call pose build and refine ran for 0.001 secs (0.001u,0.s) (success)
Tactic call fast_conj ran for 0.001 secs (0.001u,0.s) (success)
Tactic call abstract-fast_conj ran for 0.001 secs (0.001u,0.s) (success)
Tactic call close-abstract ran for 0. secs (0.u,0.s)
Params: n= 3
Tactic call refine ran for 0. secs (0.u,0.s) (success)
Tactic call pose build and refine ran for 0. secs (0.u,0.s) (success)
Tactic call fast_conj ran for 0. secs (0.u,0.s) (success)
Tactic call abstract-fast_conj ran for 0. secs (0.u,0.s) (success)
Tactic call abstract-fast_conj ran for 0.001 secs (0.001u,0.s) (success)
Tactic call close-abstract ran for 0. secs (0.u,0.s)
6 changes: 3 additions & 3 deletions coq/PerformanceExperiments/do_n_open_constr_True/_0_Sanity.log
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Params: n= 0
Tactic call open-constr-True-1000 ran for 0.027 secs (0.015u,0.011s) (success)
Tactic call open-constr-True-1000 ran for 0.021 secs (0.021u,0.s) (success)
Params: n= 1
Tactic call open-constr-True-1000 ran for 0.026 secs (0.026u,0.s) (success)
Tactic call open-constr-True-1000 ran for 0.019 secs (0.u,0.019s) (success)
Params: n= 2
Tactic call open-constr-True-1000 ran for 0.07 secs (0.065u,0.004s) (success)
Tactic call open-constr-True-1000 ran for 0.028 secs (0.028u,0.s) (success)
6 changes: 3 additions & 3 deletions coq/PerformanceExperiments/do_n_pose/_0_Sanity.log
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Params: n= 0
Tactic call do-100-pose-I ran for 0.002 secs (0.001u,0.s) (success)
Params: n= 1
Tactic call do-100-pose-I ran for 0.002 secs (0.002u,0.s) (success)
Params: n= 1
Tactic call do-100-pose-I ran for 0.008 secs (0.008u,0.s) (success)
Params: n= 2
Tactic call do-100-pose-I ran for 0.002 secs (0.002u,0.s) (success)
Tactic call do-100-pose-I ran for 0.013 secs (0.013u,0.s) (success)
4 changes: 2 additions & 2 deletions coq/PerformanceExperiments/intros_n_fun/_0_Sanity.log
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@ Tactic call abstract-intros ran for 0. secs (0.u,0.s) (success)
Tactic call close-abstract ran for 0. secs (0.u,0.s)
Params: n= 1
Tactic call intros ran for 0. secs (0.u,0.s) (success)
Tactic call abstract-intros ran for 0. secs (0.u,0.s) (success)
Tactic call close-abstract ran for 0. secs (0.u,0.s)
Tactic call abstract-intros ran for 0.002 secs (0.002u,0.s) (success)
Tactic call close-abstract ran for 0.002 secs (0.002u,0.s)
Params: n= 2
Tactic call intros ran for 0. secs (0.u,0.s) (success)
Tactic call abstract-intros ran for 0. secs (0.u,0.s) (success)
Expand Down
6 changes: 3 additions & 3 deletions coq/PerformanceExperiments/iota_reduction_with_abstract_fact8/_0_Sanity.log
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
Params: a-n= 0 , fact-n= 8
Tactic call beta-iota-slow ran for 0. secs (0.u,0.s)
Tactic call unify-beta-iota-slow ran for 0. secs (0.u,0.s) (success)
Tactic call abstract-unify-beta-iota-slow ran for 0.155 secs (0.155u,0.s) (success)
Tactic call abstract-unify-beta-iota-slow ran for 0.591 secs (0.591u,0.s) (success)
Params: a-n= 1 , fact-n= 8
Tactic call beta-iota-slow ran for 0. secs (0.u,0.s)
Tactic call unify-beta-iota-slow ran for 0. secs (0.u,0.s) (success)
Tactic call abstract-unify-beta-iota-slow ran for 0.156 secs (0.156u,0.s) (success)
Tactic call abstract-unify-beta-iota-slow ran for 0.505 secs (0.505u,0.s) (success)
Params: a-n= 2 , fact-n= 8
Tactic call beta-iota-slow ran for 0. secs (0.u,0.s)
Tactic call unify-beta-iota-slow ran for 0. secs (0.u,0.s) (success)
Tactic call abstract-unify-beta-iota-slow ran for 0.158 secs (0.158u,0.s) (success)
Tactic call abstract-unify-beta-iota-slow ran for 0.583 secs (0.583u,0.s) (success)
4 changes: 2 additions & 2 deletions coq/PerformanceExperiments/iota_reduction_with_abstract_fact8/_1_Sanity.log
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,10 @@ Tactic call beta-iota-fast ran for 0. secs (0.u,0.s)
Tactic call unify-beta-iota-fast ran for 0. secs (0.u,0.s) (success)
Tactic call abstract-unify-beta-iota-fast ran for 0. secs (0.u,0.s) (success)
Params: a-n= 1 , fact-n= 8
Tactic call beta-iota-fast ran for 0. secs (0.u,0.s)
Tactic call beta-iota-fast ran for 0.002 secs (0.002u,0.s)
Tactic call unify-beta-iota-fast ran for 0. secs (0.u,0.s) (success)
Tactic call abstract-unify-beta-iota-fast ran for 0. secs (0.u,0.s) (success)
Params: a-n= 2 , fact-n= 8
Tactic call beta-iota-fast ran for 0. secs (0.u,0.s)
Tactic call unify-beta-iota-fast ran for 0. secs (0.u,0.s) (success)
Tactic call unify-beta-iota-fast ran for 0.002 secs (0.002u,0.s) (success)
Tactic call abstract-unify-beta-iota-fast ran for 0. secs (0.u,0.s) (success)
8 changes: 4 additions & 4 deletions coq/PerformanceExperiments/iota_reduction_with_abstract_fact9/_0_Sanity.log
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
Params: a-n= 0 , fact-n= 9
Tactic call beta-iota-slow ran for 0. secs (0.u,0.s)
Tactic call unify-beta-iota-slow ran for 0. secs (0.u,0.s) (success)
Tactic call abstract-unify-beta-iota-slow ran for 1.826 secs (1.818u,0.007s) (success)
Tactic call abstract-unify-beta-iota-slow ran for 4.178 secs (4.118u,0.059s) (success)
Params: a-n= 1 , fact-n= 9
Tactic call beta-iota-slow ran for 0. secs (0.u,0.s)
Tactic call unify-beta-iota-slow ran for 0. secs (0.u,0.s) (success)
Tactic call abstract-unify-beta-iota-slow ran for 1.748 secs (1.748u,0.s) (success)
Tactic call abstract-unify-beta-iota-slow ran for 3.245 secs (3.245u,0.s) (success)
Params: a-n= 2 , fact-n= 9
Tactic call beta-iota-slow ran for 0. secs (0.u,0.s)
Tactic call unify-beta-iota-slow ran for 0. secs (0.u,0.s) (success)
Tactic call abstract-unify-beta-iota-slow ran for 1.773 secs (1.773u,0.s) (success)
Tactic call unify-beta-iota-slow ran for 0.002 secs (0.002u,0.s) (success)
Tactic call abstract-unify-beta-iota-slow ran for 3.08 secs (3.079u,0.s) (success)
64 changes: 32 additions & 32 deletions coq/PerformanceExperiments/lift_identity_evar_subst_binders/_0_Sanity.log
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,51 +1,51 @@
Params: a-extra-binders= 1 , nevars= 1000 , ctx-size= 100
Tactic call make_fun-ev ran for 0. secs (0.u,0.s)
Tactic call make_evars ran for 0.03 secs (0.03u,0.s)
Tactic call make_evars ran for 0.075 secs (0.075u,0.s)
Tactic call open_constr_F-ev ran for 0. secs (0.u,0.s)
Tactic call open_constr_FX-ev ran for 0.056 secs (0.056u,0.s)
Tactic call open_constr_FX-ev ran for 0.048 secs (0.048u,0.s)
Tactic call beta-F-ev ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-ev ran for 0.005 secs (0.005u,0.s)
Tactic call deta-id-FX-ev ran for 0.005 secs (0.005u,0.s)
Tactic call beta-FX-ev ran for 0.009 secs (0.009u,0.s)
Tactic call prebeta-FX-ev ran for 0.036 secs (0.036u,0.s)
Tactic call deta-id-FX-ev ran for 0.051 secs (0.041u,0.009s)
Tactic call beta-FX-ev ran for 0.108 secs (0.108u,0.s)
Tactic call make_fun-tt ran for 0. secs (0.u,0.s)
Tactic call make_tts ran for 0.044 secs (0.044u,0.s)
Tactic call make_tts ran for 0.084 secs (0.084u,0.s)
Tactic call open_constr_F-tt ran for 0. secs (0.u,0.s)
Tactic call open_constr_FX-tt ran for 0.01 secs (0.01u,0.s)
Tactic call open_constr_FX-tt ran for 0.029 secs (0.029u,0.s)
Tactic call beta-F-tt ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-tt ran for 0. secs (0.u,0.s)
Tactic call deta-id-FX-tt ran for 0. secs (0.u,0.s)
Tactic call beta-FX-tt ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-tt ran for 0.002 secs (0.002u,0.s)
Tactic call deta-id-FX-tt ran for 0.004 secs (0.004u,0.s)
Tactic call beta-FX-tt ran for 0.002 secs (0.002u,0.s)
Params: a-extra-binders= 2 , nevars= 1000 , ctx-size= 100
Tactic call make_fun-ev ran for 0. secs (0.u,0.s)
Tactic call make_evars ran for 0.03 secs (0.03u,0.s)
Tactic call make_evars ran for 0.141 secs (0.141u,0.s)
Tactic call open_constr_F-ev ran for 0. secs (0.u,0.s)
Tactic call open_constr_FX-ev ran for 0.057 secs (0.057u,0.s)
Tactic call open_constr_FX-ev ran for 0.048 secs (0.048u,0.s)
Tactic call beta-F-ev ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-ev ran for 0.006 secs (0.006u,0.s)
Tactic call deta-id-FX-ev ran for 0.005 secs (0.005u,0.s)
Tactic call beta-FX-ev ran for 0.006 secs (0.006u,0.s)
Tactic call make_fun-tt ran for 0. secs (0.u,0.s)
Tactic call make_tts ran for 0.043 secs (0.043u,0.s)
Tactic call prebeta-FX-ev ran for 0.035 secs (0.035u,0.s)
Tactic call deta-id-FX-ev ran for 0.03 secs (0.03u,0.s)
Tactic call beta-FX-ev ran for 0.072 secs (0.072u,0.s)
Tactic call make_fun-tt ran for 0.002 secs (0.002u,0.s)
Tactic call make_tts ran for 0.082 secs (0.082u,0.s)
Tactic call open_constr_F-tt ran for 0. secs (0.u,0.s)
Tactic call open_constr_FX-tt ran for 0.009 secs (0.009u,0.s)
Tactic call open_constr_FX-tt ran for 0.022 secs (0.022u,0.s)
Tactic call beta-F-tt ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-tt ran for 0. secs (0.u,0.s)
Tactic call deta-id-FX-tt ran for 0. secs (0.u,0.s)
Tactic call beta-FX-tt ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-tt ran for 0.004 secs (0.004u,0.s)
Tactic call deta-id-FX-tt ran for 0.002 secs (0.002u,0.s)
Tactic call beta-FX-tt ran for 0.001 secs (0.001u,0.s)
Params: a-extra-binders= 3 , nevars= 1000 , ctx-size= 100
Tactic call make_fun-ev ran for 0. secs (0.u,0.s)
Tactic call make_evars ran for 0.03 secs (0.03u,0.s)
Tactic call make_fun-ev ran for 0.002 secs (0.002u,0.s)
Tactic call make_evars ran for 0.072 secs (0.072u,0.s)
Tactic call open_constr_F-ev ran for 0. secs (0.u,0.s)
Tactic call open_constr_FX-ev ran for 0.056 secs (0.056u,0.s)
Tactic call open_constr_FX-ev ran for 0.032 secs (0.032u,0.s)
Tactic call beta-F-ev ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-ev ran for 0.006 secs (0.006u,0.s)
Tactic call deta-id-FX-ev ran for 0.005 secs (0.005u,0.s)
Tactic call beta-FX-ev ran for 0.007 secs (0.007u,0.s)
Tactic call prebeta-FX-ev ran for 0.026 secs (0.026u,0.s)
Tactic call deta-id-FX-ev ran for 0.034 secs (0.034u,0.s)
Tactic call beta-FX-ev ran for 0.086 secs (0.086u,0.s)
Tactic call make_fun-tt ran for 0. secs (0.u,0.s)
Tactic call make_tts ran for 0.043 secs (0.043u,0.s)
Tactic call make_tts ran for 0.097 secs (0.097u,0.s)
Tactic call open_constr_F-tt ran for 0. secs (0.u,0.s)
Tactic call open_constr_FX-tt ran for 0.009 secs (0.009u,0.s)
Tactic call open_constr_FX-tt ran for 0.031 secs (0.031u,0.s)
Tactic call beta-F-tt ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-tt ran for 0. secs (0.u,0.s)
Tactic call deta-id-FX-tt ran for 0. secs (0.u,0.s)
Tactic call beta-FX-tt ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-tt ran for 0.002 secs (0.002u,0.s)
Tactic call deta-id-FX-tt ran for 0.003 secs (0.003u,0.s)
Tactic call beta-FX-tt ran for 0.001 secs (0.001u,0.s)
72 changes: 36 additions & 36 deletions coq/PerformanceExperiments/lift_identity_evar_subst_ctx/_0_Sanity.log
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,51 +1,51 @@
Params: a-ctx-size= 1 , nevars= 1000 , extra-binders= 100
Tactic call make_fun-ev ran for 0.012 secs (0.012u,0.s)
Tactic call make_evars ran for 0.017 secs (0.014u,0.003s)
Tactic call make_fun-ev ran for 0.031 secs (0.031u,0.s)
Tactic call make_evars ran for 0.049 secs (0.049u,0.s)
Tactic call open_constr_F-ev ran for 0. secs (0.u,0.s)
Tactic call open_constr_FX-ev ran for 0.021 secs (0.02u,0.s)
Tactic call open_constr_FX-ev ran for 0.015 secs (0.015u,0.s)
Tactic call beta-F-ev ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-ev ran for 0. secs (0.u,0.s)
Tactic call deta-id-FX-ev ran for 0. secs (0.u,0.s)
Tactic call beta-FX-ev ran for 0. secs (0.u,0.s)
Tactic call make_fun-tt ran for 0.024 secs (0.024u,0.s)
Tactic call make_tts ran for 0.018 secs (0.018u,0.s)
Tactic call prebeta-FX-ev ran for 0.002 secs (0.u,0.002s)
Tactic call deta-id-FX-ev ran for 0.001 secs (0.u,0.001s)
Tactic call beta-FX-ev ran for 0.005 secs (0.003u,0.002s)
Tactic call make_fun-tt ran for 0.012 secs (0.012u,0.s)
Tactic call make_tts ran for 0.065 secs (0.065u,0.s)
Tactic call open_constr_F-tt ran for 0. secs (0.u,0.s)
Tactic call open_constr_FX-tt ran for 0.006 secs (0.006u,0.s)
Tactic call open_constr_FX-tt ran for 0.021 secs (0.021u,0.s)
Tactic call beta-F-tt ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-tt ran for 0. secs (0.u,0.s)
Tactic call deta-id-FX-tt ran for 0. secs (0.u,0.s)
Tactic call beta-FX-tt ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-tt ran for 0.002 secs (0.002u,0.s)
Tactic call deta-id-FX-tt ran for 0.004 secs (0.004u,0.s)
Tactic call beta-FX-tt ran for 0.003 secs (0.003u,0.s)
Params: a-ctx-size= 2 , nevars= 1000 , extra-binders= 100
Tactic call make_fun-ev ran for 0.012 secs (0.012u,0.s)
Tactic call make_evars ran for 0.017 secs (0.017u,0.s)
Tactic call make_fun-ev ran for 0.022 secs (0.022u,0.s)
Tactic call make_evars ran for 0.043 secs (0.043u,0.s)
Tactic call open_constr_F-ev ran for 0. secs (0.u,0.s)
Tactic call open_constr_FX-ev ran for 0.019 secs (0.019u,0.s)
Tactic call open_constr_FX-ev ran for 0.027 secs (0.027u,0.s)
Tactic call beta-F-ev ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-ev ran for 0. secs (0.u,0.s)
Tactic call deta-id-FX-ev ran for 0. secs (0.u,0.s)
Tactic call beta-FX-ev ran for 0. secs (0.u,0.s)
Tactic call make_fun-tt ran for 0.023 secs (0.023u,0.s)
Tactic call make_tts ran for 0.018 secs (0.018u,0.s)
Tactic call prebeta-FX-ev ran for 0.006 secs (0.006u,0.s)
Tactic call deta-id-FX-ev ran for 0.004 secs (0.004u,0.s)
Tactic call beta-FX-ev ran for 0.006 secs (0.u,0.006s)
Tactic call make_fun-tt ran for 0.027 secs (0.027u,0.s)
Tactic call make_tts ran for 0.058 secs (0.058u,0.s)
Tactic call open_constr_F-tt ran for 0. secs (0.u,0.s)
Tactic call open_constr_FX-tt ran for 0.006 secs (0.006u,0.s)
Tactic call open_constr_FX-tt ran for 0.021 secs (0.021u,0.s)
Tactic call beta-F-tt ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-tt ran for 0. secs (0.u,0.s)
Tactic call deta-id-FX-tt ran for 0. secs (0.u,0.s)
Tactic call beta-FX-tt ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-tt ran for 0.001 secs (0.001u,0.s)
Tactic call deta-id-FX-tt ran for 0.003 secs (0.003u,0.s)
Tactic call beta-FX-tt ran for 0.001 secs (0.001u,0.s)
Params: a-ctx-size= 3 , nevars= 1000 , extra-binders= 100
Tactic call make_fun-ev ran for 0.012 secs (0.012u,0.s)
Tactic call make_evars ran for 0.017 secs (0.017u,0.s)
Tactic call make_fun-ev ran for 0.029 secs (0.029u,0.s)
Tactic call make_evars ran for 0.07 secs (0.07u,0.s)
Tactic call open_constr_F-ev ran for 0. secs (0.u,0.s)
Tactic call open_constr_FX-ev ran for 0.02 secs (0.02u,0.s)
Tactic call open_constr_FX-ev ran for 0.025 secs (0.025u,0.s)
Tactic call beta-F-ev ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-ev ran for 0. secs (0.u,0.s)
Tactic call deta-id-FX-ev ran for 0. secs (0.u,0.s)
Tactic call beta-FX-ev ran for 0. secs (0.u,0.s)
Tactic call make_fun-tt ran for 0.025 secs (0.025u,0.s)
Tactic call make_tts ran for 0.018 secs (0.018u,0.s)
Tactic call prebeta-FX-ev ran for 0.007 secs (0.007u,0.s)
Tactic call deta-id-FX-ev ran for 0.004 secs (0.004u,0.s)
Tactic call beta-FX-ev ran for 0.006 secs (0.006u,0.s)
Tactic call make_fun-tt ran for 0.027 secs (0.027u,0.s)
Tactic call make_tts ran for 0.063 secs (0.063u,0.s)
Tactic call open_constr_F-tt ran for 0. secs (0.u,0.s)
Tactic call open_constr_FX-tt ran for 0.006 secs (0.006u,0.s)
Tactic call open_constr_FX-tt ran for 0.024 secs (0.016u,0.007s)
Tactic call beta-F-tt ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-tt ran for 0. secs (0.u,0.s)
Tactic call deta-id-FX-tt ran for 0. secs (0.u,0.s)
Tactic call beta-FX-tt ran for 0. secs (0.u,0.s)
Tactic call prebeta-FX-tt ran for 0.005 secs (0.005u,0.s)
Tactic call deta-id-FX-tt ran for 0.002 secs (0.002u,0.s)
Tactic call beta-FX-tt ran for 0.002 secs (0.002u,0.s)
Loading
Loading