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

AttributeError: 'Values' object has no attribute 'pep_references' #37

Closed
JasonGross opened this issue Apr 19, 2021 · 14 comments
Closed

AttributeError: 'Values' object has no attribute 'pep_references' #37

JasonGross opened this issue Apr 19, 2021 · 14 comments

Comments

@JasonGross
Copy link
Contributor 

AttributeError: 'Values' object has no attribute 'pep_references'
Exiting due to error.  Use "--traceback" to diagnose.
Please report errors to <docutils-users@lists.sf.net>.
Include "--traceback" output, Docutils version (0.17.1 [release]),
Python version (3.7.3), your OS type & version, and the
command line used.
make: *** [Makefile:1004: alectryon-html-done.timestamp] Error 1

https://github.com/HoTT/HoTT/runs/2369972229#step:6:2123

Is it safe to always run with --traceback? Is it suggested?
@JasonGross
Copy link
Contributor Author

Maybe it's not so nondeterministic, it seems to happen every time now.

Traceback (most recent call last):
  File "etc/alectryon/alectryon.py", line 26, in <module>
    main()
  File "/github/workspace/etc/alectryon/alectryon/cli.py", line 662, in main
    process_pipelines(args)
  File "/github/workspace/etc/alectryon/alectryon/cli.py", line 651, in process_pipelines
    state = call_pipeline_step(step, state, ctx)
  File "/github/workspace/etc/alectryon/alectryon/cli.py", line 620, in call_pipeline_step
    return step(state, **{p: ctx[p] for p in params})
  File "/github/workspace/etc/alectryon/alectryon/cli.py", line 114, in gen_rstcoq_html
    RSTCoqParser, RSTCoqStandaloneReader)
  File "/github/workspace/etc/alectryon/alectryon/cli.py", line 105, in _gen_docutils_html
    enable_exit_status=True).decode("utf-8")
  File "/home/coq/.local/lib/python3.7/site-packages/docutils/core.py", line 417, in publish_string
    enable_exit_status=enable_exit_status)
  File "/home/coq/.local/lib/python3.7/site-packages/docutils/core.py", line 665, in publish_programmatically
    output = pub.publish(enable_exit_status=enable_exit_status)
  File "/home/coq/.local/lib/python3.7/site-packages/docutils/core.py", line 218, in publish
    self.settings)
  File "/home/coq/.local/lib/python3.7/site-packages/docutils/readers/__init__.py", line 72, in read
    self.parse()
  File "/home/coq/.local/lib/python3.7/site-packages/docutils/readers/__init__.py", line 78, in parse
    self.parser.parse(self.input, document)
  File "/github/workspace/etc/alectryon/alectryon/docutils.py", line 495, in parse
    self.statemachine.run(lines, document, inliner=self.inliner)
  File "/home/coq/.local/lib/python3.7/site-packages/docutils/parsers/rst/states.py", line 158, in run
    inliner.init_customizations(document.settings)
  File "/home/coq/.local/lib/python3.7/site-packages/docutils/parsers/rst/states.py", line 607, in init_customizations
    if settings.pep_references:
AttributeError: 'Values' object has no attribute 'pep_references'
make: *** [Makefile:1005: alectryon-html-done.timestamp] Error 1

https://github.com/HoTT/HoTT/runs/2386323130?check_suite_focus=true#step:6:2122
HoTT/Coq-HoTT#1466

@JasonGross JasonGross changed the title Nondeterministic failure AttributeError: 'Values' object has no attribute 'pep_references' Apr 20, 2021
@JasonGross
Copy link
Contributor Author

Is there a way to get the python traceback to also print function arguments?

@JasonGross JasonGross mentioned this issue Apr 20, 2021
Merged
@JasonGross
Copy link
Contributor Author

Traceback with arguments: https://github.com/HoTT/HoTT/runs/2393729047?check_suite_focus=true#step:6:2122

@JasonGross
Copy link
Contributor Author

And here's the tail of the full traceback 
  File "/github/workspace/etc/alectryon/alectryon/cli.py", line 621, in call_pipeline_step
    return step(state, **{p: ctx[p] for p in params})
    ctx = {'fpath': './theories/Basics.v', 'fname': 'Basics.v', 'input': ['./theories/Basics.v', './theories/Basics/Notations.v', './theories/Basics/Utf8.v', './theories/Basics/Overture.v', './theories/Basics/PathGroupoids.v', './theories/Basics/UniverseLevel.v', './theories/Basics/Contractible.v', './theories/Basics/Equivalences.v', './theories/Basics/Decidable.v', './theories/Basics/Datatypes.v', './theories/Basics/Logic.v', './theories/Basics/Tactics.v', './theories/Basics/Nat.v', './theories/Basics/Trunc.v', './theories/Basics/Numeral.v', './theories/Basics/Decimal.v', './theories/Basics/Hexadecimal.v', './theories/WildCat.v', './theories/WildCat/Core.v', './theories/WildCat/UnitCat.v', './theories/WildCat/EmptyCat.v', './theories/WildCat/Prod.v', './theories/WildCat/Equiv.v', './theories/WildCat/Sum.v', './theories/WildCat/Forall.v', './theories/WildCat/Sigma.v', './theories/WildCat/Opposite.v', './theories/WildCat/Paths.v', './theories/WildCat/Type.v', './theories/WildCat/Induced.v', './theories/WildCat/EquivGpd.v', './theories/WildCat/FunctorCat.v', './theories/WildCat/Yoneda.v', './theories/WildCat/TwoOneCat.v', './theories/WildCat/NatTrans.v', './theories/WildCat/PointedCat.v', './theories/WildCat/Square.v', './theories/Types.v', './theories/Types/Paths.v', './theories/Types/Unit.v', './theories/Types/Forall.v', './theories/Types/Arrow.v', './theories/Types/Sigma.v', './theories/Types/Prod.v', './theories/Types/Empty.v', './theories/Types/Bool.v', './theories/Types/Sum.v', './theories/Types/Wtype.v', './theories/Types/Equiv.v', './theories/Types/Universe.v', './theories/Cubical.v', './theories/Cubical/DPath.v', './theories/Cubical/PathSquare.v', './theories/Cubical/DPathSquare.v', './theories/Cubical/PathCube.v', './theories/Cubical/DPathCube.v', './theories/Spaces/Nat.v', './theories/Spaces/List.v', './theories/Spaces/Cantor.v', './theories/Spaces/Finite/Fin.v', './theories/Spaces/Finite/FinNat.v', './theories/Spaces/Finite/FinInduction.v', './theories/Spaces/Finite/Finite.v', './theories/Spaces/Finite/FinSeq.v', './theories/Spaces/Finite/Tactics.v', './theories/Spaces/Finite.v', './theories/Spaces/Universe.v', './theories/Spaces/Card.v', './theories/Spaces/Circle.v', './theories/Spaces/TwoSphere.v', './theories/Spaces/Spheres.v', './theories/Spaces/Int.v', './theories/Spaces/Int/Core.v', './theories/Spaces/Int/Spec.v', './theories/Spaces/Int/Equiv.v', './theories/Spaces/Int/LoopExp.v', './theories/Spaces/Pos.v', './theories/Spaces/Pos/Core.v', './theories/Spaces/Pos/Spec.v', './theories/Spaces/BAut.v', './theories/Spaces/BAut/Cantor.v', './theories/Spaces/BAut/Bool.v', './theories/Spaces/BAut/Bool/IncoherentIdempotent.v', './theories/Spaces/BAut/Rigid.v', './theories/Spaces/No.v', './theories/Spaces/No/Core.v', './theories/Spaces/No/Negation.v', './theories/Spaces/No/Addition.v', './theories/Spaces/Torus/Torus.v', './theories/Spaces/Torus/TorusEquivCircles.v', './theories/Spaces/Torus/TorusHomotopy.v', './theories/Modalities/ReflectiveSubuniverse.v', './theories/Modalities/Modality.v', './theories/Modalities/Accessible.v', './theories/Modalities/Descent.v', './theories/Modalities/Separated.v', './theories/Modalities/Lex.v', './theories/Modalities/Topological.v', './theories/Modalities/Notnot.v', './theories/Modalities/Identity.v', './theories/Modalities/Localization.v', './theories/Modalities/Nullification.v', './theories/Modalities/Open.v', './theories/Modalities/Closed.v', './theories/Modalities/Fracture.v', './theories/Modalities/CoreflectiveSubuniverse.v', './theories/HIT/Coeq.v', './theories/HIT/FreeIntQuotient.v', './theories/HIT/Flattening.v', './theories/HIT/Interval.v', './theories/HIT/epi.v', './theories/HIT/unique_choice.v', './theories/HIT/surjective_factor.v', './theories/HIT/quotient.v', './theories/HIT/iso.v', './theories/HIT/SetCone.v', './theories/HIT/V.v', './theories/Limits/Limit.v', './theories/Limits/Equalizer.v', './theories/Limits/Pullback.v', './theories/Colimits/Pushout.v', './theories/Colimits/SpanPushout.v', './theories/Colimits/MappingCylinder.v', './theories/Colimits/Quotient.v', './theories/Colimits/Colimit.v', './theories/Colimits/Colimit_Sigma.v', './theories/Colimits/Colimit_Prod.v', './theories/Colimits/Colimit_Pushout.v', './theories/Colimits/Colimit_Coequalizer.v', './theories/Colimits/Colimit_Flattening.v', './theories/Colimits/Colimit_Pushout_Flattening.v', './theories/Colimits/Sequential.v', './theories/Diagrams/Graph.v', './theories/Diagrams/Diagram.v', './theories/Diagrams/Cone.v', './theories/Diagrams/Cocone.v', './theories/Diagrams/DDiagram.v', './theories/Diagrams/ConstantDiagram.v', './theories/Diagrams/CommutativeSquares.v', './theories/Diagrams/Sequence.v', './theories/Diagrams/Span.v', './theories/Diagrams/ParallelPair.v', './theories/Truncations.v', './theories/Truncations/Core.v', './theories/Truncations/Connectedness.v', './theories/Equiv/BiInv.v', './theories/Equiv/PathSplit.v', './theories/Equiv/Relational.v', './theories/BoundedSearch.v', './theories/HFiber.v', './theories/HProp.v', './theories/Extensions.v', './theories/HSet.v', './theories/Projective.v', './theories/TruncType.v', './theories/DProp.v', './theories/EquivGroupoids.v', './theories/Functorish.v', './theories/FunextAxiom.v', './theories/UnivalenceAxiom.v', './theories/ObjectClassifier.v', './theories/NullHomotopy.v', './theories/Idempotents.v', './theories/Factorization.v', './theories/Constant.v', './theories/ExcludedMiddle.v', './theories/Misc.v', './theories/PathAny.v', './theories/Utf8.v', './theories/HoTT.v', './theories/Tests.v', './theories/Metatheory/Core.v', './theories/Metatheory/FunextVarieties.v', './theories/Metatheory/TruncImpliesFunext.v', './theories/Metatheory/IntervalImpliesFunext.v', './theories/Metatheory/UnivalenceImpliesFunext.v', './theories/Metatheory/UnivalenceVarieties.v', './theories/Homotopy/HomotopyGroup.v', './theories/Homotopy/Pi1S1.v', './theories/Homotopy/Suspension.v', './theories/Homotopy/Smash.v', './theories/Homotopy/Wedge.v', './theories/Homotopy/Join.v', './theories/Homotopy/WhiteheadsPrinciple.v', './theories/Homotopy/HSpace.v', './theories/Homotopy/HSpaceS1.v', './theories/Homotopy/BlakersMassey.v', './theories/Homotopy/Freudenthal.v', './theories/Homotopy/ClassifyingSpace.v', './theories/Homotopy/EMSpace.v', './theories/Homotopy/CayleyDickson.v', './theories/Homotopy/SuccessorStructure.v', './theories/Homotopy/ExactSequence.v', './theories/Pointed.v', './theories/Pointed/Core.v', './theories/Pointed/Loops.v', './theories/Pointed/pMap.v', './theories/Pointed/pFiber.v', './theories/Pointed/pEquiv.v', './theories/Pointed/pTrunc.v', './theories/Pointed/pHomotopy.v', './theories/Pointed/pSusp.v', './theories/Spectra/Spectrum.v', './theories/Spectra/Coinductive.v', './theories/Algebra/Universal/Algebra.v', './theories/Algebra/Universal/Homomorphism.v', './theories/Algebra/Universal/Operation.v', './theories/Algebra/Universal/Congruence.v', './theories/Algebra/Universal/TermAlgebra.v', './theories/Algebra/ooGroup.v', './theories/Algebra/Aut.v', './theories/Algebra/ooAction.v', './theories/Algebra/Congruence.v', './theories/Algebra/Rings.v', './theories/Algebra/Rings/CRing.v', './theories/Algebra/Rings/Ideal.v', './theories/Algebra/Rings/QuotientRing.v', './theories/Algebra/Rings/Z.v', './theories/Algebra/AbGroups.v', './theories/Algebra/AbGroups/AbelianGroup.v', './theories/Algebra/AbGroups/Abelianization.v', './theories/Algebra/AbGroups/AbPullback.v', './theories/Algebra/AbGroups/AbPushout.v', './theories/Algebra/AbGroups/Z.v', './theories/Algebra/Groups.v', './theories/Algebra/Groups/Group.v', './theories/Algebra/Groups/Subgroup.v', './theories/Algebra/Groups/QuotientGroup.v', './theories/Algebra/Groups/Image.v', './theories/Algebra/Groups/Kernel.v', './theories/Algebra/Groups/GrpPullback.v', './theories/Algebra/Groups/FreeProduct.v', './theories/Algebra/Groups/GroupCoeq.v', './theories/Algebra/Groups/Presentation.v', './theories/Algebra/Groups/ShortExactSequence.v', './theories/Algebra/Groups/FreeGroup.v', './theories/Algebra/Groups/FreeGroup/ListQuotient.v', './theories/Algebra/Groups/FreeGroup/LoopSusp.v', './theories/Tactics.v', './theories/Tactics/BinderApply.v', './theories/Tactics/EquivalenceInduction.v', './theories/Tactics/EvalIn.v', './theories/Tactics/Nameless.v', './theories/Tactics/RewriteModuloAssociativity.v', './theories/PropResizing/PropResizing.v', './theories/PropResizing/ImpredicativeTruncation.v', './theories/PropResizing/Nat.v', './theories/Classes/tactics/ring_tac.v', './theories/Classes/tactics/ring_quote.v', './theories/Classes/tactics/ring_pol.v', './theories/Classes/isomorphisms/rings.v', './theories/Classes/orders/rings.v', './theories/Classes/orders/maps.v', './theories/Classes/orders/semirings.v', './theories/Classes/orders/dec_fields.v', './theories/Classes/orders/sum.v', './theories/Classes/orders/lattices.v', './theories/Classes/orders/naturals.v', './theories/Classes/orders/orders.v', './theories/Classes/orders/nat_int.v', './theories/Classes/orders/integers.v', './theories/Classes/orders/archimedean.v', './theories/Classes/orders/fields.v', './theories/Classes/implementations/assume_rationals.v', './theories/Classes/implementations/peano_naturals.v', './theories/Classes/implementations/binary_naturals.v', './theories/Classes/implementations/natpair_integers.v', './theories/Classes/implementations/field_of_fractions.v', './theories/Classes/implementations/list.v', './theories/Classes/implementations/bool.v', './theories/Classes/implementations/hprop_lattice.v', './theories/Classes/implementations/pointwise.v', './theories/Classes/implementations/family_prod.v', './theories/Classes/implementations/ne_list.v', './theories/Classes/interfaces/monad.v', './theories/Classes/interfaces/abstract_algebra.v', './theories/Classes/interfaces/naturals.v', './theories/Classes/interfaces/rationals.v', './theories/Classes/interfaces/canonical_names.v', './theories/Classes/interfaces/orders.v', './theories/Classes/interfaces/archimedean.v', './theories/Classes/interfaces/cauchy.v', './theories/Classes/interfaces/round.v', './theories/Classes/interfaces/integers.v', './theories/Classes/interfaces/ua_algebra.v', './theories/Classes/interfaces/ua_setalgebra.v', './theories/Classes/interfaces/ua_congruence.v', './theories/Classes/theory/premetric.v', './theories/Classes/theory/int_abs.v', './theories/Classes/theory/rings.v', './theories/Classes/theory/additional_operations.v', './theories/Classes/theory/apartness.v', './theories/Classes/theory/dec_fields.v', './theories/Classes/theory/lattices.v', './theories/Classes/theory/naturals.v', './theories/Classes/theory/nat_distance.v', './theories/Classes/theory/groups.v', './theories/Classes/theory/fields.v', './theories/Classes/theory/rationals.v', './theories/Classes/theory/integers.v', './theories/Classes/theory/ua_homomorphism.v', './theories/Classes/theory/ua_isomorphic.v', './theories/Classes/theory/ua_prod_algebra.v', './theories/Classes/theory/ua_subalgebra.v', './theories/Classes/theory/ua_quotient_algebra.v', './theories/Classes/theory/ua_first_isomorphism.v', './theories/Classes/theory/ua_second_isomorphism.v', './theories/Classes/theory/ua_third_isomorphism.v', './theories/Classes/categories/ua_category.v', './theories/Classes/tests/ring_tac.v', './theories/Analysis/Locator.v', './theories/Categories.v', './theories/Categories/Category.v', './theories/Categories/Functor.v', './theories/Categories/NaturalTransformation.v', './theories/Categories/Category/Core.v', './theories/Categories/Functor/Core.v', './theories/Categories/NaturalTransformation/Core.v', './theories/Categories/Category/Morphisms.v', './theories/Categories/Category/Strict.v', './theories/Categories/Category/Univalent.v', './theories/Categories/Category/Objects.v', './theories/Categories/Category/Dual.v', './theories/Categories/Category/Paths.v', './theories/Categories/Category/Prod.v', './theories/Categories/Category/Pi.v', './theories/Categories/Category/Sum.v', './theories/Categories/Category/Sigma.v', './theories/Categories/Category/Sigma/Core.v', './theories/Categories/Functor/Composition.v', './theories/Categories/Functor/Composition/Core.v', './theories/Categories/Functor/Identity.v', './theories/Categories/Functor/Paths.v', './theories/Categories/Category/Sigma/OnMorphisms.v', './theories/Categories/Category/Sigma/OnObjects.v', './theories/Categories/Category/Sigma/Univalent.v', './theories/Categories/Category/Subcategory.v', './theories/Categories/Category/Subcategory/Full.v', './theories/Categories/Category/Subcategory/Wide.v', './theories/Categories/Category/Notations.v', './theories/Categories/Category/Utf8.v', './theories/Categories/Functor/Prod.v', './theories/Categories/Functor/Dual.v', './theories/Categories/SetCategory.v', './theories/Categories/SetCategory/Core.v', './theories/Categories/SetCategory/Morphisms.v', './theories/Categories/SetCategory/Functors.v', './theories/Categories/SetCategory/Functors/SetProp.v', './theories/Categories/SimplicialSets.v', './theories/Categories/SemiSimplicialSets.v', './theories/Categories/FundamentalPreGroupoidCategory.v', './theories/Categories/HomotopyPreCategory.v', './theories/Categories/HomFunctor.v', './theories/Categories/Functor/Attributes.v', './theories/Categories/NaturalTransformation/Paths.v', './theories/Categories/NaturalTransformation/Identity.v', './theories/Categories/NaturalTransformation/Composition.v', './theories/Categories/NaturalTransformation/Composition/Core.v', './theories/Categories/NaturalTransformation/Composition/Laws.v', './theories/Categories/FunctorCategory.v', './theories/Categories/FunctorCategory/Core.v', './theories/Categories/NaturalTransformation/Composition/Functorial.v', './theories/Categories/ExponentialLaws.v', './theories/Categories/ExponentialLaws/Law0.v', './theories/Categories/ExponentialLaws/Law1.v', './theories/Categories/ExponentialLaws/Law1/Functors.v', './theories/Categories/ExponentialLaws/Law1/Law.v', './theories/Categories/ExponentialLaws/Law2.v', './theories/Categories/ExponentialLaws/Law2/Functors.v', './theories/Categories/ExponentialLaws/Law2/Law.v', './theories/Categories/ExponentialLaws/Law3.v', './theories/Categories/ExponentialLaws/Law3/Functors.v', './theories/Categories/ExponentialLaws/Law3/Law.v', './theories/Categories/ExponentialLaws/Law4.v', './theories/Categories/ExponentialLaws/Law4/Functors.v', './theories/Categories/ExponentialLaws/Law4/Law.v', './theories/Categories/ExponentialLaws/Tactics.v', './theories/Categories/Functor/Composition/Functorial.v', './theories/Categories/Functor/Composition/Functorial/Core.v', './theories/Categories/Functor/Composition/Functorial/Attributes.v', './theories/Categories/Functor/Composition/Laws.v', './theories/Categories/Functor/Sum.v', './theories/Categories/Functor/Pointwise.v', './theories/Categories/Functor/Prod/Core.v', './theories/Categories/Functor/Prod/Universal.v', './theories/Categories/GroupoidCategory.v', './theories/Categories/GroupoidCategory/Core.v', './theories/Categories/GroupoidCategory/Dual.v', './theories/Categories/CategoryOfGroupoids.v', './theories/Categories/DiscreteCategory.v', './theories/Categories/IndiscreteCategory.v', './theories/Categories/NatCategory.v', './theories/Categories/ChainCategory.v', './theories/Categories/InitialTerminalCategory.v', './theories/Categories/InitialTerminalCategory/Core.v', './theories/Categories/InitialTerminalCategory/Functors.v', './theories/Categories/InitialTerminalCategory/NaturalTransformations.v', './theories/Categories/InitialTerminalCategory/Pseudofunctors.v', './theories/Categories/InitialTerminalCategory/Notations.v', './theories/Categories/NaturalTransformation/Prod.v', './theories/Categories/Functor/Prod/Functorial.v', './theories/Categories/Functor/Pointwise/Core.v', './theories/Categories/Functor/Pointwise/Properties.v', './theories/Categories/Functor/Notations.v', './theories/Categories/Functor/Utf8.v', './theories/Categories/NaturalTransformation/Dual.v', './theories/Categories/NaturalTransformation/Sum.v', './theories/Categories/NaturalTransformation/Pointwise.v', './theories/Categories/FunctorCategory/Dual.v', './theories/Categories/FunctorCategory/Morphisms.v', './theories/Categories/NaturalTransformation/Isomorphisms.v', './theories/Categories/NaturalTransformation/Notations.v', './theories/Categories/NaturalTransformation/Utf8.v', './theories/Categories/Structure.v', './theories/Categories/Structure/Core.v', './theories/Categories/Structure/IdentityPrinciple.v', './theories/Categories/Structure/Notations.v', './theories/Categories/Structure/Utf8.v', './theories/Categories/CategoryOfSections.v', './theories/Categories/CategoryOfSections/Core.v', './theories/Categories/Profunctor/Core.v', './theories/Categories/Profunctor/Identity.v', './theories/Categories/Comma.v', './theories/Categories/Comma/Core.v', './theories/Categories/Adjoint.v', './theories/Categories/Adjoint/UnitCounit.v', './theories/Categories/Adjoint/Core.v', './theories/Categories/Adjoint/Paths.v', './theories/Categories/Adjoint/Identity.v', './theories/Categories/Adjoint/Composition.v', './theories/Categories/Adjoint/Composition/Core.v', './theories/Categories/Adjoint/Composition/LawsTactic.v', './theories/Categories/Adjoint/Composition/AssociativityLaw.v', './theories/Categories/Adjoint/Composition/IdentityLaws.v', './theories/Categories/Adjoint/Dual.v', './theories/Categories/Adjoint/UnitCounitCoercions.v', './theories/Categories/Adjoint/UniversalMorphisms.v', './theories/Categories/Adjoint/UniversalMorphisms/Core.v', './theories/Categories/Adjoint/Functorial.v', './theories/Categories/Adjoint/Functorial/Core.v', './theories/Categories/Adjoint/Functorial/Parts.v', './theories/Categories/Adjoint/Functorial/Laws.v', './theories/Categories/Adjoint/Hom.v', './theories/Categories/Adjoint/HomCoercions.v', './theories/Categories/Adjoint/Pointwise.v', './theories/Categories/Adjoint/Notations.v', './theories/Categories/Adjoint/Utf8.v', './theories/Categories/Cat.v', './theories/Categories/Cat/Core.v', './theories/Categories/DualFunctor.v', './theories/Categories/FunctorCategory/Functorial.v', './theories/Categories/FunctorCategory/Notations.v', './theories/Categories/FunctorCategory/Utf8.v', './theories/Categories/ProductLaws.v', './theories/Categories/GroupoidCategory/Morphisms.v', './theories/Categories/Profunctor.v', './theories/Categories/Profunctor/Representable.v', './theories/Categories/Profunctor/Notations.v', './theories/Categories/Profunctor/Utf8.v', './theories/Categories/Yoneda.v', './theories/Categories/Cat/Morphisms.v', './theories/Categories/Comma/Dual.v', './theories/Categories/Comma/Projection.v', './theories/Categories/Comma/InducedFunctors.v', './theories/Categories/Comma/ProjectionFunctors.v', './theories/Categories/Comma/Functorial.v', './theories/Categories/Comma/Notations.v', './theories/Categories/Comma/Utf8.v', './theories/Categories/Pseudofunctor.v', './theories/Categories/Pseudofunctor/Core.v', './theories/Categories/Pseudofunctor/RewriteLaws.v', './theories/Categories/Pseudofunctor/FromFunctor.v', './theories/Categories/Pseudofunctor/Identity.v', './theories/Categories/PseudonaturalTransformation.v', './theories/Categories/PseudonaturalTransformation/Core.v', './theories/Categories/LaxComma.v', './theories/Categories/LaxComma/Core.v', './theories/Categories/LaxComma/CoreParts.v', './theories/Categories/LaxComma/CoreLaws.v', './theories/Categories/LaxComma/Notations.v', './theories/Categories/LaxComma/Utf8.v', './theories/Categories/Grothendieck.v', './theories/Categories/Grothendieck/ToSet.v', './theories/Categories/Grothendieck/ToSet/Core.v', './theories/Categories/Grothendieck/ToSet/Morphisms.v', './theories/Categories/Grothendieck/ToSet/Univalent.v', './theories/Categories/Grothendieck/PseudofunctorToCat.v', './theories/Categories/Grothendieck/ToCat.v', './theories/Categories/DependentProduct.v', './theories/Categories/UniversalProperties.v', './theories/Categories/KanExtensions.v', './theories/Categories/KanExtensions/Core.v', './theories/Categories/KanExtensions/Functors.v', './theories/Categories/Limits.v', './theories/Categories/Limits/Core.v', './theories/Categories/Limits/Functors.v', './theories/Categories/Notations.v', './theories/Categories/Utf8.v', './contrib/HoTTBook.v', './contrib/HoTTBookExercises.v'], 'stdin_filename': None, 'frontend': 'coq+rst', 'backend': 'webpage', 'output': None, 'output_directory': 'alectryon-html', 'copy_fn': <function copy at 0x7fafa4e2fbf8>, 'cache_directory': 'alectryon-cache', 'include_banner': 'True', 'include_vernums': True, 'webpage_style': 'centered', 'mark_point': (None, None), 'sertop_args': ['--no_prelude', '--indices-matter', '-R', './theories,HoTT', '-Q', './contrib,HoTT.Contrib'], 'coq_args_I': [], 'coq_args_Q': [['./contrib', 'HoTT.Contrib']], 'coq_args_R': [['./theories', 'HoTT']], 'debug': False, 'traceback': True, 'point': None, 'marker': None, 'html_assets': ['alectryon.js', 'alectryon.css', 'docutils_basic.css', 'tango_subtle.css', 'tango_subtle.min.css'], 'html_classes': [], 'pipelines': [('./theories/Basics.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Basics/Notations.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Basics/Utf8.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Basics/Overture.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Basics/PathGroupoids.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Basics/UniverseLevel.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Basics/Contractible.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Basics/Equivalences.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Basics/Decidable.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Basics/Datatypes.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Basics/Logic.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Basics/Tactics.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Basics/Nat.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Basics/Trunc.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Basics/Numeral.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Basics/Decimal.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Basics/Hexadecimal.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/UnitCat.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/EmptyCat.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Prod.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Equiv.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Sum.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Forall.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Sigma.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Opposite.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Paths.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Type.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Induced.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/EquivGpd.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/FunctorCat.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Yoneda.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/TwoOneCat.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/NatTrans.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/PointedCat.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Square.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Types.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Types/Paths.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Types/Unit.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Types/Forall.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Types/Arrow.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Types/Sigma.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Types/Prod.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Types/Empty.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Types/Bool.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Types/Sum.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Types/Wtype.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Types/Equiv.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Types/Universe.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Cubical.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Cubical/DPath.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Cubical/PathSquare.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Cubical/DPathSquare.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Cubical/PathCube.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Cubical/DPathCube.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Nat.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/List.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Cantor.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Finite/Fin.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Finite/FinNat.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Finite/FinInduction.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Finite/Finite.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Finite/FinSeq.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Finite/Tactics.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Finite.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Universe.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Card.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Circle.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/TwoSphere.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Spheres.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Int.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Int/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Int/Spec.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Int/Equiv.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Int/LoopExp.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Pos.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Pos/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Pos/Spec.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/BAut.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/BAut/Cantor.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/BAut/Bool.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/BAut/Bool/IncoherentIdempotent.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/BAut/Rigid.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/No.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/No/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/No/Negation.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/No/Addition.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Torus/Torus.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Torus/TorusEquivCircles.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Torus/TorusHomotopy.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Modalities/ReflectiveSubuniverse.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Modality.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Accessible.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Descent.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Separated.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Lex.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Topological.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Notnot.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Identity.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Localization.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Nullification.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Open.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Closed.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Fracture.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Modalities/CoreflectiveSubuniverse.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/HIT/Coeq.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/HIT/FreeIntQuotient.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/HIT/Flattening.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/HIT/Interval.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/HIT/epi.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/HIT/unique_choice.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/HIT/surjective_factor.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/HIT/quotient.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/HIT/iso.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/HIT/SetCone.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/HIT/V.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Limits/Limit.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Limits/Equalizer.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Limits/Pullback.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Pushout.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Colimits/SpanPushout.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Colimits/MappingCylinder.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Quotient.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Colimit.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Colimit_Sigma.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Colimit_Prod.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Colimit_Pushout.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Colimit_Coequalizer.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Colimit_Flattening.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Colimit_Pushout_Flattening.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Sequential.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/Graph.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/Diagram.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/Cone.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/Cocone.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/DDiagram.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/ConstantDiagram.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/CommutativeSquares.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/Sequence.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/Span.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/ParallelPair.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Truncations.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Truncations/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Truncations/Connectedness.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Equiv/BiInv.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Equiv/PathSplit.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Equiv/Relational.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/BoundedSearch.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/HFiber.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/HProp.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Extensions.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/HSet.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Projective.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/TruncType.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/DProp.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/EquivGroupoids.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Functorish.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/FunextAxiom.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/UnivalenceAxiom.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/ObjectClassifier.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/NullHomotopy.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Idempotents.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Factorization.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Constant.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/ExcludedMiddle.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Misc.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/PathAny.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Utf8.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/HoTT.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Tests.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Metatheory/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Metatheory/FunextVarieties.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Metatheory/TruncImpliesFunext.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Metatheory/IntervalImpliesFunext.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Metatheory/UnivalenceImpliesFunext.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Metatheory/UnivalenceVarieties.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/HomotopyGroup.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/Pi1S1.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/Suspension.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/Smash.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/Wedge.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/Join.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/WhiteheadsPrinciple.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/HSpace.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/HSpaceS1.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/BlakersMassey.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/Freudenthal.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/ClassifyingSpace.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/EMSpace.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/CayleyDickson.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/SuccessorStructure.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/ExactSequence.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Pointed.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Pointed/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Pointed/Loops.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Pointed/pMap.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Pointed/pFiber.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Pointed/pEquiv.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Pointed/pTrunc.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Pointed/pHomotopy.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Pointed/pSusp.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spectra/Spectrum.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Spectra/Coinductive.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Universal/Algebra.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Universal/Homomorphism.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Universal/Operation.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Universal/Congruence.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Universal/TermAlgebra.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/ooGroup.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Aut.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/ooAction.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Congruence.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Rings.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Rings/CRing.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Rings/Ideal.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Rings/QuotientRing.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Rings/Z.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/AbGroups.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/AbGroups/AbelianGroup.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/AbGroups/Abelianization.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/AbGroups/AbPullback.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/AbGroups/AbPushout.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/AbGroups/Z.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/Group.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/Subgroup.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/QuotientGroup.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/Image.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/Kernel.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/GrpPullback.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/FreeProduct.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/GroupCoeq.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/Presentation.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/ShortExactSequence.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/FreeGroup.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/FreeGroup/ListQuotient.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/FreeGroup/LoopSusp.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Tactics.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Tactics/BinderApply.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Tactics/EquivalenceInduction.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Tactics/EvalIn.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Tactics/Nameless.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Tactics/RewriteModuloAssociativity.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/PropResizing/PropResizing.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/PropResizing/ImpredicativeTruncation.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/PropResizing/Nat.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/tactics/ring_tac.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/tactics/ring_quote.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/tactics/ring_pol.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/isomorphisms/rings.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/rings.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/maps.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/semirings.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/dec_fields.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/sum.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/lattices.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/naturals.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/orders.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/nat_int.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/integers.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/archimedean.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/fields.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/assume_rationals.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/peano_naturals.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/binary_naturals.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/natpair_integers.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/field_of_fractions.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/list.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/bool.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/hprop_lattice.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/pointwise.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/family_prod.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/ne_list.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/monad.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/abstract_algebra.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/naturals.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/rationals.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/canonical_names.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/orders.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/archimedean.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/cauchy.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/round.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/integers.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/ua_algebra.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/ua_setalgebra.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/ua_congruence.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/premetric.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/int_abs.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/rings.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/additional_operations.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/apartness.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/dec_fields.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/lattices.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/naturals.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/nat_distance.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/groups.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/fields.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/rationals.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/integers.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/ua_homomorphism.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/ua_isomorphic.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/ua_prod_algebra.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/ua_subalgebra.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/ua_quotient_algebra.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/ua_first_isomorphism.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/ua_second_isomorphism.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/ua_third_isomorphism.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/categories/ua_category.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Classes/tests/ring_tac.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Analysis/Locator.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Morphisms.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Strict.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Univalent.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Objects.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Dual.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Paths.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Prod.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Pi.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Sum.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Sigma.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Sigma/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Composition.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Composition/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Identity.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Paths.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Sigma/OnMorphisms.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Sigma/OnObjects.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Sigma/Univalent.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Subcategory.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Subcategory/Full.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Subcategory/Wide.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Notations.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Utf8.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Prod.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Dual.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/SetCategory.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/SetCategory/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/SetCategory/Morphisms.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/SetCategory/Functors.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/SetCategory/Functors/SetProp.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/SimplicialSets.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/SemiSimplicialSets.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/FundamentalPreGroupoidCategory.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/HomotopyPreCategory.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/HomFunctor.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Attributes.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Paths.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Identity.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Composition.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Composition/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Composition/Laws.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/FunctorCategory.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/FunctorCategory/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Composition/Functorial.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law0.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law1.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law1/Functors.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law1/Law.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law2.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law2/Functors.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law2/Law.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law3.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law3/Functors.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law3/Law.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law4.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law4/Functors.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law4/Law.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Tactics.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Composition/Functorial.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Composition/Functorial/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Composition/Functorial/Attributes.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Composition/Laws.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Sum.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Pointwise.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Prod/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Prod/Universal.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/GroupoidCategory.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/GroupoidCategory/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/GroupoidCategory/Dual.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/CategoryOfGroupoids.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/DiscreteCategory.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/IndiscreteCategory.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/NatCategory.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ChainCategory.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/InitialTerminalCategory.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/InitialTerminalCategory/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/InitialTerminalCategory/Functors.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/InitialTerminalCategory/NaturalTransformations.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/InitialTerminalCategory/Pseudofunctors.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/InitialTerminalCategory/Notations.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Prod.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Prod/Functorial.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Pointwise/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Pointwise/Properties.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Notations.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Utf8.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Dual.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Sum.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Pointwise.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/FunctorCategory/Dual.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/FunctorCategory/Morphisms.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Isomorphisms.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Notations.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Utf8.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Structure.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Structure/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Structure/IdentityPrinciple.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Structure/Notations.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Structure/Utf8.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/CategoryOfSections.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/CategoryOfSections/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Profunctor/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Profunctor/Identity.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/UnitCounit.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Paths.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Identity.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Composition.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Composition/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Composition/LawsTactic.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Composition/AssociativityLaw.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Composition/IdentityLaws.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Dual.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/UnitCounitCoercions.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/UniversalMorphisms.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/UniversalMorphisms/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Functorial.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Functorial/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Functorial/Parts.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Functorial/Laws.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Hom.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/HomCoercions.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Pointwise.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Notations.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Utf8.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Cat.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Cat/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/DualFunctor.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/FunctorCategory/Functorial.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/FunctorCategory/Notations.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/FunctorCategory/Utf8.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/ProductLaws.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/GroupoidCategory/Morphisms.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Profunctor.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Profunctor/Representable.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Profunctor/Notations.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Profunctor/Utf8.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Yoneda.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Cat/Morphisms.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma/Dual.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma/Projection.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma/InducedFunctors.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma/ProjectionFunctors.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma/Functorial.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma/Notations.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma/Utf8.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Pseudofunctor.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Pseudofunctor/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Pseudofunctor/RewriteLaws.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Pseudofunctor/FromFunctor.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Pseudofunctor/Identity.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/PseudonaturalTransformation.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/PseudonaturalTransformation/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/LaxComma.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/LaxComma/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/LaxComma/CoreParts.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/LaxComma/CoreLaws.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/LaxComma/Notations.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/LaxComma/Utf8.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Grothendieck.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Grothendieck/ToSet.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Grothendieck/ToSet/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Grothendieck/ToSet/Morphisms.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Grothendieck/ToSet/Univalent.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Grothendieck/PseudofunctorToCat.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Grothendieck/ToCat.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/DependentProduct.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/UniversalProperties.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/KanExtensions.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/KanExtensions/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/KanExtensions/Functors.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Limits.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Limits/Core.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Limits/Functors.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Notations.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./theories/Categories/Utf8.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./contrib/HoTTBook.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>)), ('./contrib/HoTTBookExercises.v', (<function read_plain at 0x7fafa5025d90>, <function register_docutils at 0x7fafa4e3a400>, <function gen_rstcoq_html at 0x7fafa4e3a510>, <function copy_assets at 0x7fafa4e3abf8>, <function write_file.<locals>.<lambda> at 0x7fafa4e3b7b8>))]}
    params = ['fpath', 'webpage_style', 'include_banner', 'include_vernums', 'html_assets', 'traceback']
    state = 'Require Export Basics.Notations.\nRequire Export Basics.Overture.\nRequire Export Basics.UniverseLevel.\nRequire Export Basics.PathGroupoids.\nRequire Export Basics.Contractible.\nRequire Export Basics.Equivalences.\nRequire Export Basics.Trunc.\nRequire Export Basics.Decidable.\nRequire Export Basics.Utf8.\nRequire Export Basics.Tactics.\n\nRequire Export Basics.Nat.\nRequire Export Basics.Numeral.\n'
    step = <function gen_rstcoq_html at 0x7fafa4e3a510>

  File "/github/workspace/etc/alectryon/alectryon/cli.py", line 115, in gen_rstcoq_html
    document = <document: >
    inliner = <docutils.parsers.rst.states.Inliner object at 0x7fafa42cae10>
    input_lines = StringList(['.. coq::', '', '   Require Export Basics.Notations.', '   Require Export Basics.Overture.', '   Require Export Basics.UniverseLevel.', '   Require Export Basics.PathGroupoids.', '   Require Export Basics.Contractible.', '   Require Export Basics.Equivalences.', '   Require Export Basics.Trunc.', '   Require Export Basics.Decidable.', '   Require Export Basics.Utf8.', '   Require Export Basics.Tactics.', '', '   Require Export Basics.Nat.', '   Require Export Basics.Numeral.', ''], items=[('./theories/Basics.v', 0), ('./theories/Basics.v', 0), ('./theories/Basics.v', 0), ('./theories/Basics.v', 1), ('./theories/Basics.v', 2), ('./theories/Basics.v', 3), ('./theories/Basics.v', 4), ('./theories/Basics.v', 5), ('./theories/Basics.v', 6), ('./theories/Basics.v', 7), ('./theories/Basics.v', 8), ('./theories/Basics.v', 9), ('./theories/Basics.v', 10), ('./theories/Basics.v', 11), ('./theories/Basics.v', 12), ('./theories/Basics.v', 12)])
    input_offset = 0
    match_titles = True
    self = <docutils.parsers.rst.states.RSTStateMachine object at 0x7fafa43b1ef0>

  File "/home/coq/.local/lib/python3.7/site-packages/docutils/parsers/rst/states.py", line 607, in init_customizations
    if settings.pep_references:
    args = {'self': <docutils.parsers.rst.states.Inliner object at 0x7fafa42cae10>, 'settings': <Values at 0x7fafa4427ac8: {'title': None, 'generator': None, 'datestamp': None, 'source_link': None, 'source_url': None, 'toc_backlinks': 'entry', 'footnote_backlinks': 1, 'sectnum_xform': 1, 'strip_comments': None, 'strip_elements_with_classes': None, 'strip_classes': None, 'report_level': 2, 'halt_level': 4, 'exit_status_level': 5, 'debug': None, 'warning_stream': None, 'traceback': True, 'input_encoding': 'utf-8', 'input_encoding_error_handler': 'strict', 'output_encoding': 'utf-8', 'output_encoding_error_handler': 'xmlcharrefreplace', 'error_encoding': 'utf-8', 'error_encoding_error_handler': 'backslashreplace', 'language_code': 'en', 'record_dependencies': DependencyList(None, []), 'config': None, 'id_prefix': '', 'auto_id_prefix': 'id', 'dump_settings': None, 'dump_internals': None, 'dump_transforms': None, 'dump_pseudo_xml': None, 'expose_internals': None, 'strict_visitor': None, '_disable_config': None, '_source': './theories/Basics.v', '_destination': None, '_config_files': [], 'file_insertion_enabled': 1, 'raw_enabled': 1, 'line_length_limit': 10000, 'doctitle_xform': 1, 'docinfo_xform': 1, 'sectsubtitle_xform': 0, 'webpage_style': 'centered', 'alectryon_banner': 'True', 'alectryon_vernums': True, 'template': '/home/coq/.local/lib/python3.7/site-packages/docutils/writers/html4css1/template.txt', 'stylesheet': None, 'stylesheet_path': None, 'embed_stylesheet': False, 'stylesheet_dirs': [], 'initial_header_level': '1', 'field_name_limit': 14, 'option_limit': 14, 'footnote_references': 'brackets', 'attribution': 'dash', 'compact_lists': 1, 'compact_field_lists': 1, 'embed_images': 0, 'table_style': '', 'math_output': 'HTML math.css', 'xml_declaration': 1, 'cloak_email_addresses': None}>, 'start_string_prefix': '(^|(?<=\\s|["\'(<\\[{༺༼᚛⁅⁽₍〈❨❪❬❮❰❲❴⟅⟦⟨⟪⟬⟮⦃⦅⦇⦉⦋⦍⦏⦑⦓⦕⦗⧘⧚⧼⸢⸤⸦⸨〈《「『【〔〖〘〚〝〝﴾︗︵︷︹︻︽︿﹁﹃﹇﹙﹛﹝（［｛｟｢«‘“‹⸂⸄⸉⸌⸜⸠‚„»’”›⸃⸅⸊⸍⸝⸡‛‟\\-/:֊¡·¿;·՚-՟։־׀׃׆׳״؉؊،؍؛؞؟٪-٭۔܀-܍߷-߹࠰-࠾।॥॰෴๏๚๛༄-༒྅࿐-࿔၊-၏჻፡-፨᐀᙭᙮᛫-᛭᜵᜶។-៖៘-៚᠀-᠊᥄᥅᧞᧟᨞᨟᪠-᪦᪨-᪭᭚-᭠᰻-᰿᱾᱿᳓‐-‗†-‧‰-‸※-‾⁁-⁃⁇-⁑⁓⁕-⁞⳹-⳼⳾⳿⸀⸁⸆-⸈⸋⸎-⸛⸞⸟⸪-⸮⸰⸱、-〃〜〰〽゠・꓾꓿꘍-꘏꙳꙾꛲-꛷꡴-꡷꣎꣏꣸-꣺꤮꤯꥟꧁-꧍꧞꧟꩜-꩟꫞꫟꯫︐-︖︙︰-︲﹅﹆﹉-﹌﹐-﹒﹔-﹘﹟-﹡﹣﹨﹪﹫！-＃％-＇＊，-／：；？＠＼｡､･𐄀𐄁𐎟𐏐𐡗𐤟𐤿𐩐-𐩘𐩿𐬹-𐬿𑂻𑂼𑂾-𑃁𒑰-𒑳]))', 'end_string_suffix': '($|(?=\\s|[\x00\\\\.,;!?\\-/:֊¡·¿;·՚-՟։־׀׃׆׳״؉؊،؍؛؞؟٪-٭۔܀-܍߷-߹࠰-࠾।॥॰෴๏๚๛༄-༒྅࿐-࿔၊-၏჻፡-፨᐀᙭᙮᛫-᛭᜵᜶។-៖៘-៚᠀-᠊᥄᥅᧞᧟᨞᨟᪠-᪦᪨-᪭᭚-᭠᰻-᰿᱾᱿᳓‐-‗†-‧‰-‸※-‾⁁-⁃⁇-⁑⁓⁕-⁞⳹-⳼⳾⳿⸀⸁⸆-⸈⸋⸎-⸛⸞⸟⸪-⸮⸰⸱、-〃〜〰〽゠・꓾꓿꘍-꘏꙳꙾꛲-꛷꡴-꡷꣎꣏꣸-꣺꤮꤯꥟꧁-꧍꧞꧟꩜-꩟꫞꫟꯫︐-︖︙︰-︲﹅﹆﹉-﹌﹐-﹒﹔-﹘﹟-﹡﹣﹨﹪﹫！-＃％-＇＊，-／：；？＠＼｡､･𐄀𐄁𐎟𐏐𐡗𐤟𐤿𐩐-𐩘𐩿𐬹-𐬿𑂻𑂼𑂾-𑃁𒑰-𒑳"\')>\\]}༻༽᚜⁆⁾₎〉❩❫❭❯❱❳❵⟆⟧⟩⟫⟭⟯⦄⦆⦈⦊⦌⦎⦐⦒⦔⦖⦘⧙⧛⧽⸣⸥⸧⸩〉》」』】〕〗〙〛〞〟﴿︘︶︸︺︼︾﹀﹂﹄﹈﹚﹜﹞）］｝｠｣»’”›⸃⸅⸊⸍⸝⸡‛‟«‘“‹⸂⸄⸉⸌⸜⸠‚„]))', '__module__': 'docutils.parsers.rst.states', '__doc__': '\n    Parse inline markup; call the `parse()` method.\n    ', '__init__': <function Inliner.__init__ at 0x7fafa4be2ae8>, 'init_customizations': <function Inliner.init_customizations at 0x7fafa4be2b70>, 'parse': <function Inliner.parse at 0x7fafa4be2bf8>, 'non_whitespace_before': '(?<!\\s)', 'non_whitespace_escape_before': '(?<![\\s\\x00])', 'non_unescaped_whitespace_escape_before': '(?<!(?<!\\x00)[\\s\\x00])', 'non_whitespace_after': '(?!\\s)', 'simplename': '(?:(?!_)\\w)+(?:[-._+:](?:(?!_)\\w)+)*', 'uric': "[-_.!~*'()[\\];/:@&=+$,%a-zA-Z0-9\\x00]", 'uri_end_delim': '[>]', 'urilast': '[_~*/=+a-zA-Z0-9]', 'uri_end': "(?:[_~*/=+a-zA-Z0-9]|[-_.!~*'()[\\];/:@&=+$,%a-zA-Z0-9\\x00](?=[>]))", 'emailc': "[-_!~*'{|}/#?^`&=+$%a-zA-Z0-9\\x00]", 'email_pattern': '\n          %(emailc)s+(?:\\.%(emailc)s+)*   # name\n          (?<!\\x00)@                      # at\n          %(emailc)s+(?:\\.%(emailc)s*)*   # host\n          %(uri_end)s                     # final URI char\n          ', 'quoted_start': <function Inliner.quoted_start at 0x7fafa4be2c80>, 'inline_obj': <function Inliner.inline_obj at 0x7fafa4be2d08>, 'problematic': <function Inliner.problematic at 0x7fafa4be2d90>, 'emphasis': <function Inliner.emphasis at 0x7fafa4be2e18>, 'strong': <function Inliner.strong at 0x7fafa4be2ea0>, 'interpreted_or_phrase_ref': <function Inliner.interpreted_or_phrase_ref at 0x7fafa4be2f28>, 'phrase_ref': <function Inliner.phrase_ref at 0x7fafa4bec048>, 'adjust_uri': <function Inliner.adjust_uri at 0x7fafa4bec0d0>, 'interpreted': <function Inliner.interpreted at 0x7fafa4bec158>, 'literal': <function Inliner.literal at 0x7fafa4bec1e0>, 'inline_internal_target': <function Inliner.inline_internal_target at 0x7fafa4bec268>, 'substitution_reference': <function Inliner.substitution_reference at 0x7fafa4bec2f0>, 'footnote_reference': <function Inliner.footnote_reference at 0x7fafa4bec378>, 'reference': <function Inliner.reference at 0x7fafa4bec400>, 'anonymous_reference': <function Inliner.anonymous_reference at 0x7fafa4bec488>, 'standalone_uri': <function Inliner.standalone_uri at 0x7fafa4bec510>, 'pep_reference': <function Inliner.pep_reference at 0x7fafa4bec598>, 'rfc_url': 'rfc%d.html', 'rfc_reference': <function Inliner.rfc_reference at 0x7fafa4bec620>, 'implicit_inline': <function Inliner.implicit_inline at 0x7fafa4bec6a8>, 'dispatch': {'*': <function Inliner.emphasis at 0x7fafa4be2e18>, '**': <function Inliner.strong at 0x7fafa4be2ea0>, '`': <function Inliner.interpreted_or_phrase_ref at 0x7fafa4be2f28>, '``': <function Inliner.literal at 0x7fafa4bec1e0>, '_`': <function Inliner.inline_internal_target at 0x7fafa4bec268>, ']_': <function Inliner.footnote_reference at 0x7fafa4bec378>, '|': <function Inliner.substitution_reference at 0x7fafa4bec2f0>, '_': <function Inliner.reference at 0x7fafa4bec400>, '__': <function Inliner.anonymous_reference at 0x7fafa4bec488>}, '__dict__': <attribute '__dict__' of 'Inliner' objects>, '__weakref__': <attribute '__weakref__' of 'Inliner' objects>}
    end_string_suffix = '($|(?=\\s|[\x00\\\\.,;!?\\-/:֊¡·¿;·՚-՟։־׀׃׆׳״؉؊،؍؛؞؟٪-٭۔܀-܍߷-߹࠰-࠾।॥॰෴๏๚๛༄-༒྅࿐-࿔၊-၏჻፡-፨᐀᙭᙮᛫-᛭᜵᜶។-៖៘-៚᠀-᠊᥄᥅᧞᧟᨞᨟᪠-᪦᪨-᪭᭚-᭠᰻-᰿᱾᱿᳓‐-‗†-‧‰-‸※-‾⁁-⁃⁇-⁑⁓⁕-⁞⳹-⳼⳾⳿⸀⸁⸆-⸈⸋⸎-⸛⸞⸟⸪-⸮⸰⸱、-〃〜〰〽゠・꓾꓿꘍-꘏꙳꙾꛲-꛷꡴-꡷꣎꣏꣸-꣺꤮꤯꥟꧁-꧍꧞꧟꩜-꩟꫞꫟꯫︐-︖︙︰-︲﹅﹆﹉-﹌﹐-﹒﹔-﹘﹟-﹡﹣﹨﹪﹫！-＃％-＇＊，-／：；？＠＼｡､･𐄀𐄁𐎟𐏐𐡗𐤟𐤿𐩐-𐩘𐩿𐬹-𐬿𑂻𑂼𑂾-𑃁𒑰-𒑳"\')>\\]}༻༽᚜⁆⁾₎〉❩❫❭❯❱❳❵⟆⟧⟩⟫⟭⟯⦄⦆⦈⦊⦌⦎⦐⦒⦔⦖⦘⧙⧛⧽⸣⸥⸧⸩〉》」』】〕〗〙〛〞〟﴿︘︶︸︺︼︾﹀﹂﹄﹈﹚﹜﹞）］｝｠｣»’”›⸃⸅⸊⸍⸝⸡‛‟«‘“‹⸂⸄⸉⸌⸜⸠‚„]))'
    parts = ('initial_inline', '(^|(?<=\\s|["\'(<\\[{༺༼᚛⁅⁽₍〈❨❪❬❮❰❲❴⟅⟦⟨⟪⟬⟮⦃⦅⦇⦉⦋⦍⦏⦑⦓⦕⦗⧘⧚⧼⸢⸤⸦⸨〈《「『【〔〖〘〚〝〝﴾︗︵︷︹︻︽︿﹁﹃﹇﹙﹛﹝（［｛｟｢«‘“‹⸂⸄⸉⸌⸜⸠‚„»’”›⸃⸅⸊⸍⸝⸡‛‟\\-/:֊¡·¿;·՚-՟։־׀׃׆׳״؉؊،؍؛؞؟٪-٭۔܀-܍߷-߹࠰-࠾।॥॰෴๏๚๛༄-༒྅࿐-࿔၊-၏჻፡-፨᐀᙭᙮᛫-᛭᜵᜶។-៖៘-៚᠀-᠊᥄᥅᧞᧟᨞᨟᪠-᪦᪨-᪭᭚-᭠᰻-᰿᱾᱿᳓‐-‗†-‧‰-‸※-‾⁁-⁃⁇-⁑⁓⁕-⁞⳹-⳼⳾⳿⸀⸁⸆-⸈⸋⸎-⸛⸞⸟⸪-⸮⸰⸱、-〃〜〰〽゠・꓾꓿꘍-꘏꙳꙾꛲-꛷꡴-꡷꣎꣏꣸-꣺꤮꤯꥟꧁-꧍꧞꧟꩜-꩟꫞꫟꯫︐-︖︙︰-︲﹅﹆﹉-﹌﹐-﹒﹔-﹘﹟-﹡﹣﹨﹪﹫！-＃％-＇＊，-／：；？＠＼｡､･𐄀𐄁𐎟𐏐𐡗𐤟𐤿𐩐-𐩘𐩿𐬹-𐬿𑂻𑂼𑂾-𑃁𒑰-𒑳]))', '', [('start', '', '(?!\\s)', ['\\*\\*', '\\*(?!\\*)', '``', '_`', '\\|(?!\\|)']), ('whole', '', '($|(?=\\s|[\x00\\\\.,;!?\\-/:֊¡·¿;·՚-՟։־׀׃׆׳״؉؊،؍؛؞؟٪-٭۔܀-܍߷-߹࠰-࠾।॥॰෴๏๚๛༄-༒྅࿐-࿔၊-၏჻፡-፨᐀᙭᙮᛫-᛭᜵᜶។-៖៘-៚᠀-᠊᥄᥅᧞᧟᨞᨟᪠-᪦᪨-᪭᭚-᭠᰻-᰿᱾᱿᳓‐-‗†-‧‰-‸※-‾⁁-⁃⁇-⁑⁓⁕-⁞⳹-⳼⳾⳿⸀⸁⸆-⸈⸋⸎-⸛⸞⸟⸪-⸮⸰⸱、-〃〜〰〽゠・꓾꓿꘍-꘏꙳꙾꛲-꛷꡴-꡷꣎꣏꣸-꣺꤮꤯꥟꧁-꧍꧞꧟꩜-꩟꫞꫟꯫︐-︖︙︰-︲﹅﹆﹉-﹌﹐-﹒﹔-﹘﹟-﹡﹣﹨﹪﹫！-＃％-＇＊，-／：；？＠＼｡､･𐄀𐄁𐎟𐏐𐡗𐤟𐤿𐩐-𐩘𐩿𐬹-𐬿𑂻𑂼𑂾-𑃁𒑰-𒑳"\')>\\]}༻༽᚜⁆⁾₎〉❩❫❭❯❱❳❵⟆⟧⟩⟫⟭⟯⦄⦆⦈⦊⦌⦎⦐⦒⦔⦖⦘⧙⧛⧽⸣⸥⸧⸩〉》」』】〕〗〙〛〞〟﴿︘︶︸︺︼︾﹀﹂﹄﹈﹚﹜﹞）］｝｠｣»’”›⸃⸅⸊⸍⸝⸡‛‟«‘“‹⸂⸄⸉⸌⸜⸠‚„]))', ['(?P<refname>(?:(?!_)\\w)+(?:[-._+:](?:(?!_)\\w)+)*)(?P<refend>__?)', ('footnotelabel', '\\[', '(?P<fnend>\\]_)', ['[0-9]+', '\\#((?:(?!_)\\w)+(?:[-._+:](?:(?!_)\\w)+)*)?', '\\*', '(?P<citationlabel>(?:(?!_)\\w)+(?:[-._+:](?:(?!_)\\w)+)*)'])]), ('backquote', '(?P<role>(:(?:(?!_)\\w)+(?:[-._+:](?:(?!_)\\w)+)*:)?)', '(?!\\s)', ['`(?!`)'])])
    self = <docutils.parsers.rst.states.Inliner object at 0x7fafa42cae10>
    settings = <Values at 0x7fafa4427ac8: {'title': None, 'generator': None, 'datestamp': None, 'source_link': None, 'source_url': None, 'toc_backlinks': 'entry', 'footnote_backlinks': 1, 'sectnum_xform': 1, 'strip_comments': None, 'strip_elements_with_classes': None, 'strip_classes': None, 'report_level': 2, 'halt_level': 4, 'exit_status_level': 5, 'debug': None, 'warning_stream': None, 'traceback': True, 'input_encoding': 'utf-8', 'input_encoding_error_handler': 'strict', 'output_encoding': 'utf-8', 'output_encoding_error_handler': 'xmlcharrefreplace', 'error_encoding': 'utf-8', 'error_encoding_error_handler': 'backslashreplace', 'language_code': 'en', 'record_dependencies': DependencyList(None, []), 'config': None, 'id_prefix': '', 'auto_id_prefix': 'id', 'dump_settings': None, 'dump_internals': None, 'dump_transforms': None, 'dump_pseudo_xml': None, 'expose_internals': None, 'strict_visitor': None, '_disable_config': None, '_source': './theories/Basics.v', '_destination': None, '_config_files': [], 'file_insertion_enabled': 1, 'raw_enabled': 1, 'line_length_limit': 10000, 'doctitle_xform': 1, 'docinfo_xform': 1, 'sectsubtitle_xform': 0, 'webpage_style': 'centered', 'alectryon_banner': 'True', 'alectryon_vernums': True, 'template': '/home/coq/.local/lib/python3.7/site-packages/docutils/writers/html4css1/template.txt', 'stylesheet': None, 'stylesheet_path': None, 'embed_stylesheet': False, 'stylesheet_dirs': [], 'initial_header_level': '1', 'field_name_limit': 14, 'option_limit': 14, 'footnote_references': 'brackets', 'attribution': 'dash', 'compact_lists': 1, 'compact_field_lists': 1, 'embed_images': 0, 'table_style': '', 'math_output': 'HTML math.css', 'xml_declaration': 1, 'cloak_email_addresses': None}>
    start_string_prefix = '(^|(?<=\\s|["\'(<\\[{༺༼᚛⁅⁽₍〈❨❪❬❮❰❲❴⟅⟦⟨⟪⟬⟮⦃⦅⦇⦉⦋⦍⦏⦑⦓⦕⦗⧘⧚⧼⸢⸤⸦⸨〈《「『【〔〖〘〚〝〝﴾︗︵︷︹︻︽︿﹁﹃﹇﹙﹛﹝（［｛｟｢«‘“‹⸂⸄⸉⸌⸜⸠‚„»’”›⸃⸅⸊⸍⸝⸡‛‟\\-/:֊¡·¿;·՚-՟։־׀׃׆׳״؉؊،؍؛؞؟٪-٭۔܀-܍߷-߹࠰-࠾।॥॰෴๏๚๛༄-༒྅࿐-࿔၊-၏჻፡-፨᐀᙭᙮᛫-᛭᜵᜶។-៖៘-៚᠀-᠊᥄᥅᧞᧟᨞᨟᪠-᪦᪨-᪭᭚-᭠᰻-᰿᱾᱿᳓‐-‗†-‧‰-‸※-‾⁁-⁃⁇-⁑⁓⁕-⁞⳹-⳼⳾⳿⸀⸁⸆-⸈⸋⸎-⸛⸞⸟⸪-⸮⸰⸱、-〃〜〰〽゠・꓾꓿꘍-꘏꙳꙾꛲-꛷꡴-꡷꣎꣏꣸-꣺꤮꤯꥟꧁-꧍꧞꧟꩜-꩟꫞꫟꯫︐-︖︙︰-︲﹅﹆﹉-﹌﹐-﹒﹔-﹘﹟-﹡﹣﹨﹪﹫！-＃％-＇＊，-／：；？＠＼｡､･𐄀𐄁𐎟𐏐𐡗𐤟𐤿𐩐-𐩘𐩿𐬹-𐬿𑂻𑂼𑂾-𑃁𒑰-𒑳]))'

AttributeError: 'Values' object has no attribute 'pep_references'

@JasonGross
Copy link
Contributor Author

@cpitclaudel do you have any idea what's going on here?

@cpitclaudel
Copy link
Owner

I will look soon

@cpitclaudel
Copy link
Owner

Quick check: which command is yielding this result? You're processing a .v file with embedded reST? Or with embedded Coqdoc?

@JasonGross
Copy link
Contributor Author

I'm invoking python3 etc/alectryon/alectryon.py --frontend coq+rst --backend webpage --sertop-arg=--no_prelude --sertop-arg=--indices-matter -R "./theories" HoTT -Q "./contrib" HoTT.Contrib --output-directory alectryon-html --cache-directory alectryon-cache ./theories/Basics.v ./theories/Basics/Notations.v ./theories/Basics/Utf8.v ... with a couple hundred more .v files, it looks like it's processing theories/Basics.v. I'm claiming there's embedded reST, but in fact we haven't added any yet.

@JasonGross
Copy link
Contributor Author

JasonGross commented Apr 21, 2021 •
edited
Loading

It looks like there was a similar issue in Sphinx (sphinx-doc/sphinx#4512) that was fixed by

 default_settings = {
     'embed_stylesheet': False,
     'cloak_email_addresses': True,
     'pep_base_url': 'https://www.python.org/dev/peps/',
+    'pep_references': None,
     'rfc_base_url': 'https://tools.ietf.org/html/',
+    'rfc_references': None,
     'input_encoding': 'utf-8-sig',
     'doctitle_xform': False,
     'sectsubtitle_xform': False,
     'halt_level': 5,
     'file_insertion_enabled': True,
     'smartquotes_locales': [],
 }

in sphinx/environment/__init__.py

@cpitclaudel
Copy link
Owner

Thanks, I saw that one, but I should be inheriting all default settings in RstCoqParser:

class RSTCoqParser(docutils.parsers.rst.Parser):
    """A wrapper around the reStructuredText parser for literate Coq files."""

    supported = ('coq',)
    """Aliases this parser supports."""

    settings_spec = ('Literate Coq Parser Options', None,
                     docutils.parsers.rst.Parser.settings_spec[2]) # ← Here

Which version of docutils are you using?

@cpitclaudel
Copy link
Owner

it looks like it's processing theories/Basics.v. I'm claiming there's embedded reST, but in fact we haven't added any yet.

If you run that same command manually, with just theories/Basics.v, do you get the same issue?

@cpitclaudel
Copy link
Owner

Reproduced by upgrading to 0.17

@JasonGross
Copy link
Contributor Author

That's strange, given that we seem to have succeeded on docutils-0.17 (see https://github.com/HoTT/HoTT/runs/2353352310?check_suite_focus=true), but we are failing on docutils-0.17.1. In any case, the failure occurs with docutils 0.17.1 [release] and Python version 3.7.3.

@cpitclaudel
Copy link
Owner

Ah sorry, I meant I updated to the latest from 0.16, and things are now reproducing; it could be that the culprit is 17.1 instead of 17. Will look right away.

@cpitclaudel cpitclaudel mentioned this issue Dec 18, 2021
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@JasonGross @cpitclaudel