SkySkimmer

(* next to constr_in_context *)

let () =
  define "constr_in_context_alt" (ident @-> constr @-> closure @-> tac constr) @@ fun id t c ->
  Proofview.Goal.goals >>= function
  | [gl] ->
    gl >>= fun gl ->
    let env = Proofview.Goal.env gl in
    let sigma = Proofview.Goal.sigma gl in
    let has_var =

SkySkimmer

90136317	total
7585417		./Spaces/Torus/TorusEquivCircles.vo
4570944		./Pointed/Core.vo
4353756		./Homotopy/CayleyDickson.vo
3429253		./Colimits/Sequential.vo
3414226		./Spaces/Spheres.vo
3363757		./Colimits/Colimit_Flattening.vo
3004861		./Cubical/PathCube.vo
2570380		./Homotopy/Syllepsis.vo
1323781		./Algebra/Groups/FreeProduct.vo

SkySkimmer

File "./theories/Logic/ExtensionalityFacts.v", line 95, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
FunctExt_iff_EqDeltaProjs.u1 <= Delta.u0
FunctExt_iff_EqDeltaProjs.u1 <= diagonal_projs_same_behavior.u0
FunctExt_iff_EqDeltaProjs.u1 <= FunctExt_iff_EqDeltaProjs.u0
FunctExt_iff_EqDeltaProjs.u1 = FunctExt_iff_EqDeltaProjs.u2
[private-mono,fragile,default]
File "./theories/Logic/ExtensionalityFacts.v", line 104, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
FunctExt_UniqInverse.u2 <= FunctExt_UniqInverse.u1

SkySkimmer

695 opam.NEW/ocaml-NEW/.opam-switch/build/coq-unimath.dev/UniMath/Tactics/EnsureStructuredProofs.v.prof.json.gz
718 opam.NEW/ocaml-NEW/.opam-switch/build/coq-engine-bench-lite.dev/coq/PerformanceExperiments/Ltac2Compat/Array.v.prof.json.gz
720 opam.NEW/ocaml-NEW/.opam-switch/build/coq-performance-tests-lite.dev/PerformanceExperiments/Ltac2Compat/Array.v.prof.json.gz
748 opam.NEW/ocaml-NEW/.opam-switch/build/coq-engine-bench-lite.dev/coq/PerformanceDemos/evar_creation.v.prof.json.gz
919 opam.NEW/ocaml-NEW/.opam-switch/build/coq-rewriter-perf-SuperFast.dev/src/Rewriter/Util/Tactics/Test.v.prof.json.gz
924 opam.NEW/ocaml-NEW/.opam-switch/build/coq-fiat-crypto-with-bedrock.dev/src/Util/Tactics/Test.v.prof.json.gz
926 opam.NEW/ocaml-NEW/.opam-switch/build/coq-rewriter.dev/src/Rewriter/Util/Tactics/Test.v.prof.json.gz
939 opam.NEW/ocaml-NEW/.opam-switch/build/coq-performance-tests-lite.dev/PerformanceExperiments/Reify/OCamlReify.v.prof.json.gz
951 opam.NEW/ocaml-NEW/.opam-switch/build/coq-engine-bench-lite.dev/coq/

SkySkimmer

(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-noinit" "-indices-matter" "-type-in-type" "-w" "-notation-overridden" "-w" "-deprecated-native-compiler-option" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/UniMath/UniMath" "UniMath" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "UniMath.CategoryTheory.LeftKanExtension" "-native-compiler" "no") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 688 lines to 71 lines, then from 84 lines to 800 lines, then from 799 lines to 123 lines, then from 136 lines to 646 lines, then from 650 lines to 171 lines, then from 184 lines to 570 lines, then from 572 lines to 204 lines, then from 217 lines to 880 lines, then from 884 lines to 284 lines, then from 297 lines to 626 lines, then from 630 lines to 328 lines, then from 341 lines to 1806 lines, then from 1797 lines to 365 lines, then from 375 lines to 363 lines, then from 3

SkySkimmer

(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-noinit" "-indices-matter" "-type-in-type" "-w" "-notation-overridden" "-w" "-deprecated-native-compiler-option" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/UniMath/UniMath" "UniMath" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "UniMath.CategoryTheory.LeftKanExtension" "-native-compiler" "no") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 688 lines to 71 lines, then from 84 lines to 800 lines, then from 799 lines to 123 lines, then from 136 lines to 646 lines, then from 650 lines to 171 lines, then from 184 lines to 570 lines, then from 572 lines to 204 lines, then from 217 lines to 880 lines, then from 884 lines to 284 lines, then from 297 lines to 626 lines, then from 630 lines to 328 lines, then from 341 lines to 1806 lines, then from 1797 lines to 365 lines, then from 375 lines to 363 lines, then from 3

SkySkimmer

(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-noinit" "-indices-matter" "-type-in-type" "-w" "-notation-overridden" "-w" "-deprecated-native-compiler-option" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/UniMath/UniMath" "UniMath" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "UniMath.CategoryTheory.LeftKanExtension" "-native-compiler" "no") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 688 lines to 71 lines, then from 84 lines to 800 lines, then from 799 lines to 123 lines, then from 136 lines to 646 lines, then from 650 lines to 171 lines, then from 184 lines to 570 lines, then from 572 lines to 204 lines, then from 217 lines to 880 lines, then from 884 lines to 284 lines, then from 297 lines to 626 lines, then from 630 lines to 328 lines, then from 341 lines to 1806 lines, then from 1797 lines to 365 lines *)
(* coqc version 8.18+alpha compiled with OC

SkySkimmer

Package: firefox-skyskimmer-patches
Version: 1.0
Section: custom
Priority: optional
Architecture: all
Essential: no
Maintainer: skyskimmer.net
Depends: zip, unzip, sed, coreutils
Description: Patch firefox post-install
  - disable clickselectsall behaviour in address bar

SkySkimmer

1 #NS 0 u
2 #NS 0 eq
3 #NS 0 α
1 #UP 1
0 #ES 1
4 #NS 0 a
1 #EV 0
2 #EV 1
3 #ES 0
4 #EP #BD 4 2 3

SkySkimmer

1 #NS 0 u
2 #NS 0 eq
3 #NS 0 α
1 #UP 1
0 #ES 1
4 #NS 0 a
1 #EV 0
2 #EV 1
3 #ES 0
4 #EP #BD 4 2 3