Adapt to coq/coq#19530

coq/PerformanceDemos/constr_eq.v

@@ -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

coq/PerformanceDemos/lift_identity_evar_subst.v

@@ -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

coq/PerformanceDemos/lift_non_identity_evar_subst.v

@@ -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]

coq/PerformanceDemos/quadratic_reduction.v

@@ -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).

coq/PerformanceDemos/rewrite_strat_repeated_app.v

@@ -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.
@@ -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.

coq/PerformanceDemos/rewrite_strat_under_binders.v

@@ -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.

coq/PerformanceExperiments/.coq-version

@@ -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

coq/PerformanceExperiments/Harness.v

@@ -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.

coq/PerformanceExperiments/conj_True_fast_conj/_0_Sanity.log

@@ -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)

coq/PerformanceExperiments/do_n_open_constr_True/_0_Sanity.log

@@ -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)

coq/PerformanceExperiments/do_n_pose/_0_Sanity.log

@@ -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)

coq/PerformanceExperiments/intros_n_fun/_0_Sanity.log

@@ -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)

coq/PerformanceExperiments/iota_reduction_with_abstract_fact8/_0_Sanity.log

@@ -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)

coq/PerformanceExperiments/iota_reduction_with_abstract_fact8/_1_Sanity.log

@@ -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)

coq/PerformanceExperiments/iota_reduction_with_abstract_fact9/_0_Sanity.log

@@ -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)

coq/PerformanceExperiments/lift_identity_evar_subst_binders/_0_Sanity.log

@@ -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)

coq/PerformanceExperiments/lift_identity_evar_subst_ctx/_0_Sanity.log

@@ -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)