| Index | index by Group | index by Distribution | index by Vendor | index by creation date | index by Name | Mirrors | Help | Search |
| Name: rocq-doc | Distribution: Fedora Project |
| Version: 9.2.0 | Vendor: Fedora Project |
| Release: 1.fc45 | Build date: Thu Apr 16 18:24:21 2026 |
| Group: Unspecified | Build host: buildhw-x86-13.rdu3.fedoraproject.org |
| Size: 62063259 | Source RPM: rocq-9.2.0-1.fc45.src.rpm |
| Packager: Fedora Project | |
| Url: https://rocq-prover.org/ | |
| Summary: Documentation for the Rocq proof management system | |
Rocq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. This package provides documentation and tutorials for the system. The main documentation comes in two parts: the main Library documentation, which describes all Corelib.* modules, and the Reference Manual, which gives a more complete description of the whole system. Included are HTML versions of both and a PDF version of the Reference Manual.
OPUBL-1.0 AND LGPL-2.1-only AND MIT
* Thu Apr 16 2026 Jerry James <loganjerry@gmail.com> - 9.2.0-1 - Version 9.2.0 - Drop upstreamed documentation patch - Enable the native compiler for x86_64 * Fri Mar 20 2026 Jerry James <loganjerry@gmail.com> - 9.1.1-1 - Initial RPM
/usr/share/doc/rocq /usr/share/doc/rocq/corelib /usr/share/doc/rocq/corelib/Corelib.Array.ArrayAxioms.html /usr/share/doc/rocq/corelib/Corelib.Array.PrimArray.html /usr/share/doc/rocq/corelib/Corelib.BinNums.IntDef.html /usr/share/doc/rocq/corelib/Corelib.BinNums.NatDef.html /usr/share/doc/rocq/corelib/Corelib.BinNums.PosDef.html /usr/share/doc/rocq/corelib/Corelib.Classes.CMorphisms.html /usr/share/doc/rocq/corelib/Corelib.Classes.CRelationClasses.html /usr/share/doc/rocq/corelib/Corelib.Classes.Equivalence.html /usr/share/doc/rocq/corelib/Corelib.Classes.Init.html /usr/share/doc/rocq/corelib/Corelib.Classes.Morphisms.html /usr/share/doc/rocq/corelib/Corelib.Classes.Morphisms_Prop.html /usr/share/doc/rocq/corelib/Corelib.Classes.RelationClasses.html /usr/share/doc/rocq/corelib/Corelib.Classes.SetoidTactics.html /usr/share/doc/rocq/corelib/Corelib.Compat.Coq818.html /usr/share/doc/rocq/corelib/Corelib.Compat.Coq819.html /usr/share/doc/rocq/corelib/Corelib.Compat.Coq820.html /usr/share/doc/rocq/corelib/Corelib.Compat.Rocq90.html /usr/share/doc/rocq/corelib/Corelib.Compat.Rocq91.html /usr/share/doc/rocq/corelib/Corelib.Floats.FloatAxioms.html /usr/share/doc/rocq/corelib/Corelib.Floats.FloatClass.html /usr/share/doc/rocq/corelib/Corelib.Floats.FloatOps.html /usr/share/doc/rocq/corelib/Corelib.Floats.PrimFloat.html /usr/share/doc/rocq/corelib/Corelib.Floats.SpecFloat.html /usr/share/doc/rocq/corelib/Corelib.Init.Byte.html /usr/share/doc/rocq/corelib/Corelib.Init.Datatypes.html /usr/share/doc/rocq/corelib/Corelib.Init.Decimal.html /usr/share/doc/rocq/corelib/Corelib.Init.Equality.html /usr/share/doc/rocq/corelib/Corelib.Init.Hexadecimal.html /usr/share/doc/rocq/corelib/Corelib.Init.Logic.html /usr/share/doc/rocq/corelib/Corelib.Init.Ltac.html /usr/share/doc/rocq/corelib/Corelib.Init.Nat.html /usr/share/doc/rocq/corelib/Corelib.Init.Notations.html /usr/share/doc/rocq/corelib/Corelib.Init.Number.html /usr/share/doc/rocq/corelib/Corelib.Init.Peano.html /usr/share/doc/rocq/corelib/Corelib.Init.Prelude.html /usr/share/doc/rocq/corelib/Corelib.Init.Specif.html /usr/share/doc/rocq/corelib/Corelib.Init.Sumbool.html /usr/share/doc/rocq/corelib/Corelib.Init.Tactics.html /usr/share/doc/rocq/corelib/Corelib.Init.Tauto.html /usr/share/doc/rocq/corelib/Corelib.Init.Wf.html /usr/share/doc/rocq/corelib/Corelib.Lists.ListDef.html /usr/share/doc/rocq/corelib/Corelib.Numbers.BinNums.html /usr/share/doc/rocq/corelib/Corelib.Numbers.Cyclic.Int63.CarryType.html /usr/share/doc/rocq/corelib/Corelib.Numbers.Cyclic.Int63.PrimInt63.html /usr/share/doc/rocq/corelib/Corelib.Numbers.Cyclic.Int63.Sint63Axioms.html /usr/share/doc/rocq/corelib/Corelib.Numbers.Cyclic.Int63.Uint63Axioms.html /usr/share/doc/rocq/corelib/Corelib.Program.Basics.html /usr/share/doc/rocq/corelib/Corelib.Program.Tactics.html /usr/share/doc/rocq/corelib/Corelib.Program.Utils.html /usr/share/doc/rocq/corelib/Corelib.Program.Wf.html /usr/share/doc/rocq/corelib/Corelib.Relations.Relation_Definitions.html /usr/share/doc/rocq/corelib/Corelib.Setoids.Setoid.html /usr/share/doc/rocq/corelib/Corelib.Strings.PrimString.html /usr/share/doc/rocq/corelib/Corelib.Strings.PrimStringAxioms.html /usr/share/doc/rocq/corelib/Corelib.derive.Derive.html /usr/share/doc/rocq/corelib/Corelib.extraction.ExtrHaskellBasic.html /usr/share/doc/rocq/corelib/Corelib.extraction.ExtrOcamlBasic.html /usr/share/doc/rocq/corelib/Corelib.extraction.Extraction.html /usr/share/doc/rocq/corelib/Corelib.ssr.ssrbool.html /usr/share/doc/rocq/corelib/Corelib.ssr.ssrclasses.html /usr/share/doc/rocq/corelib/Corelib.ssr.ssreflect.html /usr/share/doc/rocq/corelib/Corelib.ssr.ssrfun.html /usr/share/doc/rocq/corelib/Corelib.ssr.ssrsetoid.html /usr/share/doc/rocq/corelib/Corelib.ssr.ssrunder.html /usr/share/doc/rocq/corelib/Corelib.ssrmatching.ssrmatching.html /usr/share/doc/rocq/corelib/Ltac2.Array.html /usr/share/doc/rocq/corelib/Ltac2.Bool.html /usr/share/doc/rocq/corelib/Ltac2.Char.html /usr/share/doc/rocq/corelib/Ltac2.Compat.Coq818.html /usr/share/doc/rocq/corelib/Ltac2.Compat.Coq819.html /usr/share/doc/rocq/corelib/Ltac2.Constant.html /usr/share/doc/rocq/corelib/Ltac2.Constr.html /usr/share/doc/rocq/corelib/Ltac2.Constructor.html /usr/share/doc/rocq/corelib/Ltac2.Control.html /usr/share/doc/rocq/corelib/Ltac2.Env.html /usr/share/doc/rocq/corelib/Ltac2.Evar.html /usr/share/doc/rocq/corelib/Ltac2.FMap.html /usr/share/doc/rocq/corelib/Ltac2.FSet.html /usr/share/doc/rocq/corelib/Ltac2.Float.html /usr/share/doc/rocq/corelib/Ltac2.Fresh.html /usr/share/doc/rocq/corelib/Ltac2.Ident.html /usr/share/doc/rocq/corelib/Ltac2.Ind.html /usr/share/doc/rocq/corelib/Ltac2.Init.html /usr/share/doc/rocq/corelib/Ltac2.Int.html /usr/share/doc/rocq/corelib/Ltac2.Lazy.html /usr/share/doc/rocq/corelib/Ltac2.List.html /usr/share/doc/rocq/corelib/Ltac2.Ltac1.html /usr/share/doc/rocq/corelib/Ltac2.Ltac1CompatNotations.html /usr/share/doc/rocq/corelib/Ltac2.Ltac2.html /usr/share/doc/rocq/corelib/Ltac2.Message.html /usr/share/doc/rocq/corelib/Ltac2.Meta.html /usr/share/doc/rocq/corelib/Ltac2.Module.html /usr/share/doc/rocq/corelib/Ltac2.Notations.html /usr/share/doc/rocq/corelib/Ltac2.Option.html /usr/share/doc/rocq/corelib/Ltac2.Pattern.html /usr/share/doc/rocq/corelib/Ltac2.Printf.html /usr/share/doc/rocq/corelib/Ltac2.Proj.html /usr/share/doc/rocq/corelib/Ltac2.Pstring.html /usr/share/doc/rocq/corelib/Ltac2.RedFlags.html /usr/share/doc/rocq/corelib/Ltac2.Ref.html /usr/share/doc/rocq/corelib/Ltac2.Reference.html /usr/share/doc/rocq/corelib/Ltac2.Rewrite.html /usr/share/doc/rocq/corelib/Ltac2.Std.html /usr/share/doc/rocq/corelib/Ltac2.String.html /usr/share/doc/rocq/corelib/Ltac2.TransparentState.html /usr/share/doc/rocq/corelib/Ltac2.Uint63.html /usr/share/doc/rocq/corelib/Ltac2.Unification.html /usr/share/doc/rocq/corelib/_index.html /usr/share/doc/rocq/corelib/coqdoc.css /usr/share/doc/rocq/corelib/genindex.html /usr/share/doc/rocq/corelib/index.html /usr/share/doc/rocq/corelib/index_abbreviation_*.html /usr/share/doc/rocq/corelib/index_abbreviation_A.html /usr/share/doc/rocq/corelib/index_abbreviation_B.html /usr/share/doc/rocq/corelib/index_abbreviation_C.html /usr/share/doc/rocq/corelib/index_abbreviation_D.html /usr/share/doc/rocq/corelib/index_abbreviation_E.html /usr/share/doc/rocq/corelib/index_abbreviation_F.html /usr/share/doc/rocq/corelib/index_abbreviation_G.html /usr/share/doc/rocq/corelib/index_abbreviation_H.html /usr/share/doc/rocq/corelib/index_abbreviation_I.html /usr/share/doc/rocq/corelib/index_abbreviation_J.html /usr/share/doc/rocq/corelib/index_abbreviation_K.html /usr/share/doc/rocq/corelib/index_abbreviation_L.html /usr/share/doc/rocq/corelib/index_abbreviation_M.html /usr/share/doc/rocq/corelib/index_abbreviation_N.html /usr/share/doc/rocq/corelib/index_abbreviation_O.html /usr/share/doc/rocq/corelib/index_abbreviation_P.html /usr/share/doc/rocq/corelib/index_abbreviation_Q.html /usr/share/doc/rocq/corelib/index_abbreviation_R.html /usr/share/doc/rocq/corelib/index_abbreviation_S.html /usr/share/doc/rocq/corelib/index_abbreviation_T.html /usr/share/doc/rocq/corelib/index_abbreviation_U.html /usr/share/doc/rocq/corelib/index_abbreviation_V.html /usr/share/doc/rocq/corelib/index_abbreviation_W.html /usr/share/doc/rocq/corelib/index_abbreviation_X.html /usr/share/doc/rocq/corelib/index_abbreviation_Y.html /usr/share/doc/rocq/corelib/index_abbreviation_Z.html /usr/share/doc/rocq/corelib/index_abbreviation__.html /usr/share/doc/rocq/corelib/index_axiom_*.html /usr/share/doc/rocq/corelib/index_axiom_A.html /usr/share/doc/rocq/corelib/index_axiom_B.html /usr/share/doc/rocq/corelib/index_axiom_C.html /usr/share/doc/rocq/corelib/index_axiom_D.html /usr/share/doc/rocq/corelib/index_axiom_E.html /usr/share/doc/rocq/corelib/index_axiom_F.html /usr/share/doc/rocq/corelib/index_axiom_G.html /usr/share/doc/rocq/corelib/index_axiom_H.html /usr/share/doc/rocq/corelib/index_axiom_I.html /usr/share/doc/rocq/corelib/index_axiom_J.html /usr/share/doc/rocq/corelib/index_axiom_K.html /usr/share/doc/rocq/corelib/index_axiom_L.html /usr/share/doc/rocq/corelib/index_axiom_M.html /usr/share/doc/rocq/corelib/index_axiom_N.html /usr/share/doc/rocq/corelib/index_axiom_O.html /usr/share/doc/rocq/corelib/index_axiom_P.html /usr/share/doc/rocq/corelib/index_axiom_Q.html /usr/share/doc/rocq/corelib/index_axiom_R.html /usr/share/doc/rocq/corelib/index_axiom_S.html /usr/share/doc/rocq/corelib/index_axiom_T.html /usr/share/doc/rocq/corelib/index_axiom_U.html /usr/share/doc/rocq/corelib/index_axiom_V.html /usr/share/doc/rocq/corelib/index_axiom_W.html /usr/share/doc/rocq/corelib/index_axiom_X.html /usr/share/doc/rocq/corelib/index_axiom_Y.html /usr/share/doc/rocq/corelib/index_axiom_Z.html /usr/share/doc/rocq/corelib/index_axiom__.html /usr/share/doc/rocq/corelib/index_constructor_*.html /usr/share/doc/rocq/corelib/index_constructor_A.html /usr/share/doc/rocq/corelib/index_constructor_B.html /usr/share/doc/rocq/corelib/index_constructor_C.html /usr/share/doc/rocq/corelib/index_constructor_D.html /usr/share/doc/rocq/corelib/index_constructor_E.html /usr/share/doc/rocq/corelib/index_constructor_F.html /usr/share/doc/rocq/corelib/index_constructor_G.html /usr/share/doc/rocq/corelib/index_constructor_H.html /usr/share/doc/rocq/corelib/index_constructor_I.html /usr/share/doc/rocq/corelib/index_constructor_J.html /usr/share/doc/rocq/corelib/index_constructor_K.html /usr/share/doc/rocq/corelib/index_constructor_L.html /usr/share/doc/rocq/corelib/index_constructor_M.html /usr/share/doc/rocq/corelib/index_constructor_N.html /usr/share/doc/rocq/corelib/index_constructor_O.html /usr/share/doc/rocq/corelib/index_constructor_P.html /usr/share/doc/rocq/corelib/index_constructor_Q.html /usr/share/doc/rocq/corelib/index_constructor_R.html /usr/share/doc/rocq/corelib/index_constructor_S.html /usr/share/doc/rocq/corelib/index_constructor_T.html /usr/share/doc/rocq/corelib/index_constructor_U.html /usr/share/doc/rocq/corelib/index_constructor_V.html /usr/share/doc/rocq/corelib/index_constructor_W.html /usr/share/doc/rocq/corelib/index_constructor_X.html /usr/share/doc/rocq/corelib/index_constructor_Y.html /usr/share/doc/rocq/corelib/index_constructor_Z.html /usr/share/doc/rocq/corelib/index_constructor__.html /usr/share/doc/rocq/corelib/index_definition_*.html /usr/share/doc/rocq/corelib/index_definition_A.html /usr/share/doc/rocq/corelib/index_definition_B.html /usr/share/doc/rocq/corelib/index_definition_C.html /usr/share/doc/rocq/corelib/index_definition_D.html /usr/share/doc/rocq/corelib/index_definition_E.html /usr/share/doc/rocq/corelib/index_definition_F.html /usr/share/doc/rocq/corelib/index_definition_G.html /usr/share/doc/rocq/corelib/index_definition_H.html /usr/share/doc/rocq/corelib/index_definition_I.html /usr/share/doc/rocq/corelib/index_definition_J.html /usr/share/doc/rocq/corelib/index_definition_K.html /usr/share/doc/rocq/corelib/index_definition_L.html /usr/share/doc/rocq/corelib/index_definition_M.html /usr/share/doc/rocq/corelib/index_definition_N.html /usr/share/doc/rocq/corelib/index_definition_O.html /usr/share/doc/rocq/corelib/index_definition_P.html /usr/share/doc/rocq/corelib/index_definition_Q.html /usr/share/doc/rocq/corelib/index_definition_R.html /usr/share/doc/rocq/corelib/index_definition_S.html /usr/share/doc/rocq/corelib/index_definition_T.html /usr/share/doc/rocq/corelib/index_definition_U.html /usr/share/doc/rocq/corelib/index_definition_V.html /usr/share/doc/rocq/corelib/index_definition_W.html /usr/share/doc/rocq/corelib/index_definition_X.html /usr/share/doc/rocq/corelib/index_definition_Y.html /usr/share/doc/rocq/corelib/index_definition_Z.html /usr/share/doc/rocq/corelib/index_definition__.html /usr/share/doc/rocq/corelib/index_global_*.html /usr/share/doc/rocq/corelib/index_global_A.html /usr/share/doc/rocq/corelib/index_global_B.html /usr/share/doc/rocq/corelib/index_global_C.html /usr/share/doc/rocq/corelib/index_global_D.html /usr/share/doc/rocq/corelib/index_global_E.html /usr/share/doc/rocq/corelib/index_global_F.html /usr/share/doc/rocq/corelib/index_global_G.html /usr/share/doc/rocq/corelib/index_global_H.html /usr/share/doc/rocq/corelib/index_global_I.html /usr/share/doc/rocq/corelib/index_global_J.html /usr/share/doc/rocq/corelib/index_global_K.html /usr/share/doc/rocq/corelib/index_global_L.html /usr/share/doc/rocq/corelib/index_global_M.html /usr/share/doc/rocq/corelib/index_global_N.html /usr/share/doc/rocq/corelib/index_global_O.html /usr/share/doc/rocq/corelib/index_global_P.html /usr/share/doc/rocq/corelib/index_global_Q.html /usr/share/doc/rocq/corelib/index_global_R.html /usr/share/doc/rocq/corelib/index_global_S.html /usr/share/doc/rocq/corelib/index_global_T.html /usr/share/doc/rocq/corelib/index_global_U.html /usr/share/doc/rocq/corelib/index_global_V.html /usr/share/doc/rocq/corelib/index_global_W.html /usr/share/doc/rocq/corelib/index_global_X.html /usr/share/doc/rocq/corelib/index_global_Y.html /usr/share/doc/rocq/corelib/index_global_Z.html /usr/share/doc/rocq/corelib/index_global__.html /usr/share/doc/rocq/corelib/index_inductive_*.html /usr/share/doc/rocq/corelib/index_inductive_A.html /usr/share/doc/rocq/corelib/index_inductive_B.html /usr/share/doc/rocq/corelib/index_inductive_C.html /usr/share/doc/rocq/corelib/index_inductive_D.html /usr/share/doc/rocq/corelib/index_inductive_E.html /usr/share/doc/rocq/corelib/index_inductive_F.html /usr/share/doc/rocq/corelib/index_inductive_G.html /usr/share/doc/rocq/corelib/index_inductive_H.html /usr/share/doc/rocq/corelib/index_inductive_I.html /usr/share/doc/rocq/corelib/index_inductive_J.html /usr/share/doc/rocq/corelib/index_inductive_K.html /usr/share/doc/rocq/corelib/index_inductive_L.html /usr/share/doc/rocq/corelib/index_inductive_M.html /usr/share/doc/rocq/corelib/index_inductive_N.html /usr/share/doc/rocq/corelib/index_inductive_O.html /usr/share/doc/rocq/corelib/index_inductive_P.html /usr/share/doc/rocq/corelib/index_inductive_Q.html /usr/share/doc/rocq/corelib/index_inductive_R.html /usr/share/doc/rocq/corelib/index_inductive_S.html /usr/share/doc/rocq/corelib/index_inductive_T.html /usr/share/doc/rocq/corelib/index_inductive_U.html /usr/share/doc/rocq/corelib/index_inductive_V.html /usr/share/doc/rocq/corelib/index_inductive_W.html /usr/share/doc/rocq/corelib/index_inductive_X.html /usr/share/doc/rocq/corelib/index_inductive_Y.html /usr/share/doc/rocq/corelib/index_inductive_Z.html /usr/share/doc/rocq/corelib/index_inductive__.html /usr/share/doc/rocq/corelib/index_instance_*.html /usr/share/doc/rocq/corelib/index_instance_A.html /usr/share/doc/rocq/corelib/index_instance_B.html /usr/share/doc/rocq/corelib/index_instance_C.html /usr/share/doc/rocq/corelib/index_instance_D.html /usr/share/doc/rocq/corelib/index_instance_E.html /usr/share/doc/rocq/corelib/index_instance_F.html /usr/share/doc/rocq/corelib/index_instance_G.html /usr/share/doc/rocq/corelib/index_instance_H.html /usr/share/doc/rocq/corelib/index_instance_I.html /usr/share/doc/rocq/corelib/index_instance_J.html /usr/share/doc/rocq/corelib/index_instance_K.html /usr/share/doc/rocq/corelib/index_instance_L.html /usr/share/doc/rocq/corelib/index_instance_M.html /usr/share/doc/rocq/corelib/index_instance_N.html /usr/share/doc/rocq/corelib/index_instance_O.html /usr/share/doc/rocq/corelib/index_instance_P.html /usr/share/doc/rocq/corelib/index_instance_Q.html /usr/share/doc/rocq/corelib/index_instance_R.html /usr/share/doc/rocq/corelib/index_instance_S.html /usr/share/doc/rocq/corelib/index_instance_T.html /usr/share/doc/rocq/corelib/index_instance_U.html /usr/share/doc/rocq/corelib/index_instance_V.html /usr/share/doc/rocq/corelib/index_instance_W.html /usr/share/doc/rocq/corelib/index_instance_X.html /usr/share/doc/rocq/corelib/index_instance_Y.html /usr/share/doc/rocq/corelib/index_instance_Z.html /usr/share/doc/rocq/corelib/index_instance__.html /usr/share/doc/rocq/corelib/index_lemma_*.html /usr/share/doc/rocq/corelib/index_lemma_A.html /usr/share/doc/rocq/corelib/index_lemma_B.html /usr/share/doc/rocq/corelib/index_lemma_C.html /usr/share/doc/rocq/corelib/index_lemma_D.html /usr/share/doc/rocq/corelib/index_lemma_E.html /usr/share/doc/rocq/corelib/index_lemma_F.html /usr/share/doc/rocq/corelib/index_lemma_G.html /usr/share/doc/rocq/corelib/index_lemma_H.html /usr/share/doc/rocq/corelib/index_lemma_I.html /usr/share/doc/rocq/corelib/index_lemma_J.html /usr/share/doc/rocq/corelib/index_lemma_K.html /usr/share/doc/rocq/corelib/index_lemma_L.html /usr/share/doc/rocq/corelib/index_lemma_M.html /usr/share/doc/rocq/corelib/index_lemma_N.html /usr/share/doc/rocq/corelib/index_lemma_O.html /usr/share/doc/rocq/corelib/index_lemma_P.html /usr/share/doc/rocq/corelib/index_lemma_Q.html /usr/share/doc/rocq/corelib/index_lemma_R.html /usr/share/doc/rocq/corelib/index_lemma_S.html /usr/share/doc/rocq/corelib/index_lemma_T.html /usr/share/doc/rocq/corelib/index_lemma_U.html /usr/share/doc/rocq/corelib/index_lemma_V.html /usr/share/doc/rocq/corelib/index_lemma_W.html /usr/share/doc/rocq/corelib/index_lemma_X.html /usr/share/doc/rocq/corelib/index_lemma_Y.html /usr/share/doc/rocq/corelib/index_lemma_Z.html /usr/share/doc/rocq/corelib/index_lemma__.html /usr/share/doc/rocq/corelib/index_library_*.html /usr/share/doc/rocq/corelib/index_library_A.html /usr/share/doc/rocq/corelib/index_library_B.html /usr/share/doc/rocq/corelib/index_library_C.html /usr/share/doc/rocq/corelib/index_library_D.html /usr/share/doc/rocq/corelib/index_library_E.html /usr/share/doc/rocq/corelib/index_library_F.html /usr/share/doc/rocq/corelib/index_library_G.html /usr/share/doc/rocq/corelib/index_library_H.html /usr/share/doc/rocq/corelib/index_library_I.html /usr/share/doc/rocq/corelib/index_library_J.html /usr/share/doc/rocq/corelib/index_library_K.html /usr/share/doc/rocq/corelib/index_library_L.html /usr/share/doc/rocq/corelib/index_library_M.html /usr/share/doc/rocq/corelib/index_library_N.html /usr/share/doc/rocq/corelib/index_library_O.html /usr/share/doc/rocq/corelib/index_library_P.html /usr/share/doc/rocq/corelib/index_library_Q.html /usr/share/doc/rocq/corelib/index_library_R.html /usr/share/doc/rocq/corelib/index_library_S.html /usr/share/doc/rocq/corelib/index_library_T.html /usr/share/doc/rocq/corelib/index_library_U.html /usr/share/doc/rocq/corelib/index_library_V.html /usr/share/doc/rocq/corelib/index_library_W.html /usr/share/doc/rocq/corelib/index_library_X.html /usr/share/doc/rocq/corelib/index_library_Y.html /usr/share/doc/rocq/corelib/index_library_Z.html /usr/share/doc/rocq/corelib/index_library__.html /usr/share/doc/rocq/corelib/index_module_*.html /usr/share/doc/rocq/corelib/index_module_A.html /usr/share/doc/rocq/corelib/index_module_B.html /usr/share/doc/rocq/corelib/index_module_C.html /usr/share/doc/rocq/corelib/index_module_D.html /usr/share/doc/rocq/corelib/index_module_E.html /usr/share/doc/rocq/corelib/index_module_F.html /usr/share/doc/rocq/corelib/index_module_G.html /usr/share/doc/rocq/corelib/index_module_H.html /usr/share/doc/rocq/corelib/index_module_I.html /usr/share/doc/rocq/corelib/index_module_J.html /usr/share/doc/rocq/corelib/index_module_K.html /usr/share/doc/rocq/corelib/index_module_L.html /usr/share/doc/rocq/corelib/index_module_M.html /usr/share/doc/rocq/corelib/index_module_N.html /usr/share/doc/rocq/corelib/index_module_O.html /usr/share/doc/rocq/corelib/index_module_P.html /usr/share/doc/rocq/corelib/index_module_Q.html /usr/share/doc/rocq/corelib/index_module_R.html /usr/share/doc/rocq/corelib/index_module_S.html /usr/share/doc/rocq/corelib/index_module_T.html /usr/share/doc/rocq/corelib/index_module_U.html /usr/share/doc/rocq/corelib/index_module_V.html /usr/share/doc/rocq/corelib/index_module_W.html /usr/share/doc/rocq/corelib/index_module_X.html /usr/share/doc/rocq/corelib/index_module_Y.html /usr/share/doc/rocq/corelib/index_module_Z.html /usr/share/doc/rocq/corelib/index_module__.html /usr/share/doc/rocq/corelib/index_notation_*.html /usr/share/doc/rocq/corelib/index_notation_A.html /usr/share/doc/rocq/corelib/index_notation_B.html /usr/share/doc/rocq/corelib/index_notation_C.html /usr/share/doc/rocq/corelib/index_notation_D.html /usr/share/doc/rocq/corelib/index_notation_E.html /usr/share/doc/rocq/corelib/index_notation_F.html /usr/share/doc/rocq/corelib/index_notation_G.html /usr/share/doc/rocq/corelib/index_notation_H.html /usr/share/doc/rocq/corelib/index_notation_I.html /usr/share/doc/rocq/corelib/index_notation_J.html /usr/share/doc/rocq/corelib/index_notation_K.html /usr/share/doc/rocq/corelib/index_notation_L.html /usr/share/doc/rocq/corelib/index_notation_M.html /usr/share/doc/rocq/corelib/index_notation_N.html /usr/share/doc/rocq/corelib/index_notation_O.html /usr/share/doc/rocq/corelib/index_notation_P.html /usr/share/doc/rocq/corelib/index_notation_Q.html /usr/share/doc/rocq/corelib/index_notation_R.html /usr/share/doc/rocq/corelib/index_notation_S.html /usr/share/doc/rocq/corelib/index_notation_T.html /usr/share/doc/rocq/corelib/index_notation_U.html /usr/share/doc/rocq/corelib/index_notation_V.html /usr/share/doc/rocq/corelib/index_notation_W.html /usr/share/doc/rocq/corelib/index_notation_X.html /usr/share/doc/rocq/corelib/index_notation_Y.html /usr/share/doc/rocq/corelib/index_notation_Z.html /usr/share/doc/rocq/corelib/index_notation__.html /usr/share/doc/rocq/corelib/index_projection_*.html /usr/share/doc/rocq/corelib/index_projection_A.html /usr/share/doc/rocq/corelib/index_projection_B.html /usr/share/doc/rocq/corelib/index_projection_C.html /usr/share/doc/rocq/corelib/index_projection_D.html /usr/share/doc/rocq/corelib/index_projection_E.html /usr/share/doc/rocq/corelib/index_projection_F.html /usr/share/doc/rocq/corelib/index_projection_G.html /usr/share/doc/rocq/corelib/index_projection_H.html /usr/share/doc/rocq/corelib/index_projection_I.html /usr/share/doc/rocq/corelib/index_projection_J.html /usr/share/doc/rocq/corelib/index_projection_K.html /usr/share/doc/rocq/corelib/index_projection_L.html /usr/share/doc/rocq/corelib/index_projection_M.html /usr/share/doc/rocq/corelib/index_projection_N.html /usr/share/doc/rocq/corelib/index_projection_O.html /usr/share/doc/rocq/corelib/index_projection_P.html /usr/share/doc/rocq/corelib/index_projection_Q.html /usr/share/doc/rocq/corelib/index_projection_R.html /usr/share/doc/rocq/corelib/index_projection_S.html /usr/share/doc/rocq/corelib/index_projection_T.html /usr/share/doc/rocq/corelib/index_projection_U.html /usr/share/doc/rocq/corelib/index_projection_V.html /usr/share/doc/rocq/corelib/index_projection_W.html /usr/share/doc/rocq/corelib/index_projection_X.html /usr/share/doc/rocq/corelib/index_projection_Y.html /usr/share/doc/rocq/corelib/index_projection_Z.html /usr/share/doc/rocq/corelib/index_projection__.html /usr/share/doc/rocq/corelib/index_record_*.html /usr/share/doc/rocq/corelib/index_record_A.html /usr/share/doc/rocq/corelib/index_record_B.html /usr/share/doc/rocq/corelib/index_record_C.html /usr/share/doc/rocq/corelib/index_record_D.html /usr/share/doc/rocq/corelib/index_record_E.html /usr/share/doc/rocq/corelib/index_record_F.html /usr/share/doc/rocq/corelib/index_record_G.html /usr/share/doc/rocq/corelib/index_record_H.html /usr/share/doc/rocq/corelib/index_record_I.html /usr/share/doc/rocq/corelib/index_record_J.html /usr/share/doc/rocq/corelib/index_record_K.html /usr/share/doc/rocq/corelib/index_record_L.html /usr/share/doc/rocq/corelib/index_record_M.html /usr/share/doc/rocq/corelib/index_record_N.html /usr/share/doc/rocq/corelib/index_record_O.html /usr/share/doc/rocq/corelib/index_record_P.html /usr/share/doc/rocq/corelib/index_record_Q.html /usr/share/doc/rocq/corelib/index_record_R.html /usr/share/doc/rocq/corelib/index_record_S.html /usr/share/doc/rocq/corelib/index_record_T.html /usr/share/doc/rocq/corelib/index_record_U.html /usr/share/doc/rocq/corelib/index_record_V.html /usr/share/doc/rocq/corelib/index_record_W.html /usr/share/doc/rocq/corelib/index_record_X.html /usr/share/doc/rocq/corelib/index_record_Y.html /usr/share/doc/rocq/corelib/index_record_Z.html /usr/share/doc/rocq/corelib/index_record__.html /usr/share/doc/rocq/corelib/index_section_*.html /usr/share/doc/rocq/corelib/index_section_A.html /usr/share/doc/rocq/corelib/index_section_B.html /usr/share/doc/rocq/corelib/index_section_C.html /usr/share/doc/rocq/corelib/index_section_D.html /usr/share/doc/rocq/corelib/index_section_E.html /usr/share/doc/rocq/corelib/index_section_F.html /usr/share/doc/rocq/corelib/index_section_G.html /usr/share/doc/rocq/corelib/index_section_H.html /usr/share/doc/rocq/corelib/index_section_I.html /usr/share/doc/rocq/corelib/index_section_J.html /usr/share/doc/rocq/corelib/index_section_K.html /usr/share/doc/rocq/corelib/index_section_L.html /usr/share/doc/rocq/corelib/index_section_M.html /usr/share/doc/rocq/corelib/index_section_N.html /usr/share/doc/rocq/corelib/index_section_O.html /usr/share/doc/rocq/corelib/index_section_P.html /usr/share/doc/rocq/corelib/index_section_Q.html /usr/share/doc/rocq/corelib/index_section_R.html /usr/share/doc/rocq/corelib/index_section_S.html /usr/share/doc/rocq/corelib/index_section_T.html /usr/share/doc/rocq/corelib/index_section_U.html /usr/share/doc/rocq/corelib/index_section_V.html /usr/share/doc/rocq/corelib/index_section_W.html /usr/share/doc/rocq/corelib/index_section_X.html /usr/share/doc/rocq/corelib/index_section_Y.html /usr/share/doc/rocq/corelib/index_section_Z.html /usr/share/doc/rocq/corelib/index_section__.html /usr/share/doc/rocq/corelib/index_variable_*.html /usr/share/doc/rocq/corelib/index_variable_A.html /usr/share/doc/rocq/corelib/index_variable_B.html /usr/share/doc/rocq/corelib/index_variable_C.html /usr/share/doc/rocq/corelib/index_variable_D.html /usr/share/doc/rocq/corelib/index_variable_E.html /usr/share/doc/rocq/corelib/index_variable_F.html /usr/share/doc/rocq/corelib/index_variable_G.html /usr/share/doc/rocq/corelib/index_variable_H.html /usr/share/doc/rocq/corelib/index_variable_I.html /usr/share/doc/rocq/corelib/index_variable_J.html /usr/share/doc/rocq/corelib/index_variable_K.html /usr/share/doc/rocq/corelib/index_variable_L.html /usr/share/doc/rocq/corelib/index_variable_M.html /usr/share/doc/rocq/corelib/index_variable_N.html /usr/share/doc/rocq/corelib/index_variable_O.html /usr/share/doc/rocq/corelib/index_variable_P.html /usr/share/doc/rocq/corelib/index_variable_Q.html /usr/share/doc/rocq/corelib/index_variable_R.html /usr/share/doc/rocq/corelib/index_variable_S.html /usr/share/doc/rocq/corelib/index_variable_T.html /usr/share/doc/rocq/corelib/index_variable_U.html /usr/share/doc/rocq/corelib/index_variable_V.html /usr/share/doc/rocq/corelib/index_variable_W.html /usr/share/doc/rocq/corelib/index_variable_X.html /usr/share/doc/rocq/corelib/index_variable_Y.html /usr/share/doc/rocq/corelib/index_variable_Z.html /usr/share/doc/rocq/corelib/index_variable__.html /usr/share/doc/rocq/refman-html /usr/share/doc/rocq/refman-html/_images /usr/share/doc/rocq/refman-html/_images/async-mode.png /usr/share/doc/rocq/refman-html/_images/debugger.png /usr/share/doc/rocq/refman-html/_images/diffs-coqtop-on3.png /usr/share/doc/rocq/refman-html/_images/diffs-error-message.png /usr/share/doc/rocq/refman-html/_images/diffs-rocqide-compacted.png /usr/share/doc/rocq/refman-html/_images/diffs-rocqide-multigoal.png /usr/share/doc/rocq/refman-html/_images/diffs-rocqide-on.png /usr/share/doc/rocq/refman-html/_images/diffs-rocqide-removed.png /usr/share/doc/rocq/refman-html/_images/diffs-show-proof.png /usr/share/doc/rocq/refman-html/_images/rocqide-preferences-editor.png /usr/share/doc/rocq/refman-html/_images/rocqide-preferences-shortcuts.png /usr/share/doc/rocq/refman-html/_images/rocqide-queries.png /usr/share/doc/rocq/refman-html/_images/rocqide.png /usr/share/doc/rocq/refman-html/_sources /usr/share/doc/rocq/refman-html/_sources/addendum /usr/share/doc/rocq/refman-html/_sources/addendum/canonical-structures.rst.txt /usr/share/doc/rocq/refman-html/_sources/addendum/extended-pattern-matching.rst.txt /usr/share/doc/rocq/refman-html/_sources/addendum/extraction.rst.txt /usr/share/doc/rocq/refman-html/_sources/addendum/generalized-rewriting.rst.txt /usr/share/doc/rocq/refman-html/_sources/addendum/implicit-coercions.rst.txt /usr/share/doc/rocq/refman-html/_sources/addendum/micromega.rst.txt /usr/share/doc/rocq/refman-html/_sources/addendum/miscellaneous-extensions.rst.txt /usr/share/doc/rocq/refman-html/_sources/addendum/nsatz.rst.txt /usr/share/doc/rocq/refman-html/_sources/addendum/parallel-proof-processing.rst.txt /usr/share/doc/rocq/refman-html/_sources/addendum/program.rst.txt /usr/share/doc/rocq/refman-html/_sources/addendum/rewrite-rules.rst.txt /usr/share/doc/rocq/refman-html/_sources/addendum/ring.rst.txt /usr/share/doc/rocq/refman-html/_sources/addendum/sprop.rst.txt /usr/share/doc/rocq/refman-html/_sources/addendum/type-classes.rst.txt /usr/share/doc/rocq/refman-html/_sources/addendum/universe-polymorphism.rst.txt /usr/share/doc/rocq/refman-html/_sources/appendix /usr/share/doc/rocq/refman-html/_sources/appendix/history-and-changes /usr/share/doc/rocq/refman-html/_sources/appendix/history-and-changes/index.rst.txt /usr/share/doc/rocq/refman-html/_sources/appendix/indexes /usr/share/doc/rocq/refman-html/_sources/appendix/indexes/index.rst.txt /usr/share/doc/rocq/refman-html/_sources/changes.rst.txt /usr/share/doc/rocq/refman-html/_sources/coq-attrindex.rst.txt /usr/share/doc/rocq/refman-html/_sources/coq-cmdindex.rst.txt /usr/share/doc/rocq/refman-html/_sources/coq-exnindex.rst.txt /usr/share/doc/rocq/refman-html/_sources/coq-optindex.rst.txt /usr/share/doc/rocq/refman-html/_sources/coq-tacindex.rst.txt /usr/share/doc/rocq/refman-html/_sources/genindex.rst.txt /usr/share/doc/rocq/refman-html/_sources/history.rst.txt /usr/share/doc/rocq/refman-html/_sources/index.rst.txt /usr/share/doc/rocq/refman-html/_sources/language /usr/share/doc/rocq/refman-html/_sources/language/cic.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/coq-library.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/core /usr/share/doc/rocq/refman-html/_sources/language/core/assumptions.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/core/basic.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/core/coinductive.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/core/conversion.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/core/definitions.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/core/index.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/core/inductive.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/core/modules.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/core/primitive.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/core/records.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/core/sections.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/core/sorts.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/core/variants.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/extensions /usr/share/doc/rocq/refman-html/_sources/language/extensions/arguments-command.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/extensions/canonical.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/extensions/compil-steps.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/extensions/evars.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/extensions/implicit-arguments.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/extensions/index.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/extensions/match.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/gallina-extensions.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/gallina-specification-language.rst.txt /usr/share/doc/rocq/refman-html/_sources/language/module-system.rst.txt /usr/share/doc/rocq/refman-html/_sources/license.rst.txt /usr/share/doc/rocq/refman-html/_sources/practical-tools /usr/share/doc/rocq/refman-html/_sources/practical-tools/coq-commands.rst.txt /usr/share/doc/rocq/refman-html/_sources/practical-tools/coqide.rst.txt /usr/share/doc/rocq/refman-html/_sources/practical-tools/utilities.rst.txt /usr/share/doc/rocq/refman-html/_sources/proof-engine /usr/share/doc/rocq/refman-html/_sources/proof-engine/ltac.rst.txt /usr/share/doc/rocq/refman-html/_sources/proof-engine/ltac2.rst.txt /usr/share/doc/rocq/refman-html/_sources/proof-engine/proof-handling.rst.txt /usr/share/doc/rocq/refman-html/_sources/proof-engine/ssreflect-proof-language.rst.txt /usr/share/doc/rocq/refman-html/_sources/proof-engine/tactics.rst.txt /usr/share/doc/rocq/refman-html/_sources/proof-engine/vernacular-commands.rst.txt /usr/share/doc/rocq/refman-html/_sources/proofs /usr/share/doc/rocq/refman-html/_sources/proofs/automatic-tactics /usr/share/doc/rocq/refman-html/_sources/proofs/automatic-tactics/auto.rst.txt /usr/share/doc/rocq/refman-html/_sources/proofs/automatic-tactics/index.rst.txt /usr/share/doc/rocq/refman-html/_sources/proofs/automatic-tactics/logic.rst.txt /usr/share/doc/rocq/refman-html/_sources/proofs/creating-tactics /usr/share/doc/rocq/refman-html/_sources/proofs/creating-tactics/index.rst.txt /usr/share/doc/rocq/refman-html/_sources/proofs/writing-proofs /usr/share/doc/rocq/refman-html/_sources/proofs/writing-proofs/equality.rst.txt /usr/share/doc/rocq/refman-html/_sources/proofs/writing-proofs/index.rst.txt /usr/share/doc/rocq/refman-html/_sources/proofs/writing-proofs/proof-mode.rst.txt /usr/share/doc/rocq/refman-html/_sources/proofs/writing-proofs/reasoning-inductives.rst.txt /usr/share/doc/rocq/refman-html/_sources/proofs/writing-proofs/rewriting.rst.txt /usr/share/doc/rocq/refman-html/_sources/rocq-attrindex.rst.txt /usr/share/doc/rocq/refman-html/_sources/rocq-cmdindex.rst.txt /usr/share/doc/rocq/refman-html/_sources/rocq-exnindex.rst.txt /usr/share/doc/rocq/refman-html/_sources/rocq-optindex.rst.txt /usr/share/doc/rocq/refman-html/_sources/rocq-tacindex.rst.txt /usr/share/doc/rocq/refman-html/_sources/std-glossindex.rst.txt /usr/share/doc/rocq/refman-html/_sources/user-extensions /usr/share/doc/rocq/refman-html/_sources/user-extensions/proof-schemes.rst.txt /usr/share/doc/rocq/refman-html/_sources/user-extensions/syntax-extensions.rst.txt /usr/share/doc/rocq/refman-html/_sources/using /usr/share/doc/rocq/refman-html/_sources/using/libraries /usr/share/doc/rocq/refman-html/_sources/using/libraries/funind.rst.txt /usr/share/doc/rocq/refman-html/_sources/using/libraries/index.rst.txt /usr/share/doc/rocq/refman-html/_sources/using/libraries/writing.rst.txt /usr/share/doc/rocq/refman-html/_sources/using/tools /usr/share/doc/rocq/refman-html/_sources/using/tools/coqdoc.rst.txt /usr/share/doc/rocq/refman-html/_sources/using/tools/index.rst.txt /usr/share/doc/rocq/refman-html/_sources/zebibliography.rst.txt /usr/share/doc/rocq/refman-html/_static /usr/share/doc/rocq/refman-html/_static/RocqNotations.ttf /usr/share/doc/rocq/refman-html/_static/_sphinx_javascript_frameworks_compat.js /usr/share/doc/rocq/refman-html/_static/ansi-dark.css /usr/share/doc/rocq/refman-html/_static/ansi.css /usr/share/doc/rocq/refman-html/_static/async-mode.png /usr/share/doc/rocq/refman-html/_static/base-stemmer.js /usr/share/doc/rocq/refman-html/_static/basic.css /usr/share/doc/rocq/refman-html/_static/coqdoc.css /usr/share/doc/rocq/refman-html/_static/css /usr/share/doc/rocq/refman-html/_static/css/badge_only.css /usr/share/doc/rocq/refman-html/_static/css/custom.css /usr/share/doc/rocq/refman-html/_static/css/theme.css /usr/share/doc/rocq/refman-html/_static/debugger.png /usr/share/doc/rocq/refman-html/_static/diffs-coqtop-compacted.png /usr/share/doc/rocq/refman-html/_static/diffs-coqtop-multigoal.png /usr/share/doc/rocq/refman-html/_static/diffs-coqtop-on.png /usr/share/doc/rocq/refman-html/_static/diffs-coqtop-on3.png /usr/share/doc/rocq/refman-html/_static/diffs-error-message.png /usr/share/doc/rocq/refman-html/_static/diffs-rocqide-compacted.png /usr/share/doc/rocq/refman-html/_static/diffs-rocqide-multigoal.png /usr/share/doc/rocq/refman-html/_static/diffs-rocqide-on.png /usr/share/doc/rocq/refman-html/_static/diffs-rocqide-removed.png /usr/share/doc/rocq/refman-html/_static/diffs-show-proof.png /usr/share/doc/rocq/refman-html/_static/doctools.js /usr/share/doc/rocq/refman-html/_static/documentation_options.js /usr/share/doc/rocq/refman-html/_static/english-stemmer.js /usr/share/doc/rocq/refman-html/_static/file.png /usr/share/doc/rocq/refman-html/_static/jquery.js /usr/share/doc/rocq/refman-html/_static/js /usr/share/doc/rocq/refman-html/_static/js/badge_only.js /usr/share/doc/rocq/refman-html/_static/js/theme.js /usr/share/doc/rocq/refman-html/_static/js/versions.js /usr/share/doc/rocq/refman-html/_static/language_data.js /usr/share/doc/rocq/refman-html/_static/minus.png /usr/share/doc/rocq/refman-html/_static/notations.css /usr/share/doc/rocq/refman-html/_static/notations.js /usr/share/doc/rocq/refman-html/_static/plus.png /usr/share/doc/rocq/refman-html/_static/pre-text.css /usr/share/doc/rocq/refman-html/_static/pygments.css /usr/share/doc/rocq/refman-html/_static/rocqide-preferences-editor.png /usr/share/doc/rocq/refman-html/_static/rocqide-preferences-shortcuts.png /usr/share/doc/rocq/refman-html/_static/rocqide-queries.png /usr/share/doc/rocq/refman-html/_static/rocqide.png /usr/share/doc/rocq/refman-html/_static/rocqnotations.sty /usr/share/doc/rocq/refman-html/_static/searchtools.js /usr/share/doc/rocq/refman-html/_static/sphinx_highlight.js /usr/share/doc/rocq/refman-html/addendum /usr/share/doc/rocq/refman-html/addendum/canonical-structures.html /usr/share/doc/rocq/refman-html/addendum/extended-pattern-matching.html /usr/share/doc/rocq/refman-html/addendum/extraction.html /usr/share/doc/rocq/refman-html/addendum/generalized-rewriting.html /usr/share/doc/rocq/refman-html/addendum/implicit-coercions.html /usr/share/doc/rocq/refman-html/addendum/micromega.html /usr/share/doc/rocq/refman-html/addendum/miscellaneous-extensions.html /usr/share/doc/rocq/refman-html/addendum/nsatz.html /usr/share/doc/rocq/refman-html/addendum/parallel-proof-processing.html /usr/share/doc/rocq/refman-html/addendum/program.html /usr/share/doc/rocq/refman-html/addendum/rewrite-rules.html /usr/share/doc/rocq/refman-html/addendum/ring.html /usr/share/doc/rocq/refman-html/addendum/sprop.html /usr/share/doc/rocq/refman-html/addendum/type-classes.html /usr/share/doc/rocq/refman-html/addendum/universe-polymorphism.html /usr/share/doc/rocq/refman-html/appendix /usr/share/doc/rocq/refman-html/appendix/history-and-changes /usr/share/doc/rocq/refman-html/appendix/history-and-changes/index.html /usr/share/doc/rocq/refman-html/appendix/indexes /usr/share/doc/rocq/refman-html/appendix/indexes/index.html /usr/share/doc/rocq/refman-html/changes.html /usr/share/doc/rocq/refman-html/coq-attrindex.html /usr/share/doc/rocq/refman-html/coq-cmdindex.html /usr/share/doc/rocq/refman-html/coq-exnindex.html /usr/share/doc/rocq/refman-html/coq-optindex.html /usr/share/doc/rocq/refman-html/coq-tacindex.html /usr/share/doc/rocq/refman-html/genindex.html /usr/share/doc/rocq/refman-html/history.html /usr/share/doc/rocq/refman-html/index.html /usr/share/doc/rocq/refman-html/language /usr/share/doc/rocq/refman-html/language/cic.html /usr/share/doc/rocq/refman-html/language/coq-library.html /usr/share/doc/rocq/refman-html/language/core /usr/share/doc/rocq/refman-html/language/core/assumptions.html /usr/share/doc/rocq/refman-html/language/core/basic.html /usr/share/doc/rocq/refman-html/language/core/coinductive.html /usr/share/doc/rocq/refman-html/language/core/conversion.html /usr/share/doc/rocq/refman-html/language/core/definitions.html /usr/share/doc/rocq/refman-html/language/core/index.html /usr/share/doc/rocq/refman-html/language/core/inductive.html /usr/share/doc/rocq/refman-html/language/core/modules.html /usr/share/doc/rocq/refman-html/language/core/primitive.html /usr/share/doc/rocq/refman-html/language/core/records.html /usr/share/doc/rocq/refman-html/language/core/sections.html /usr/share/doc/rocq/refman-html/language/core/sorts.html /usr/share/doc/rocq/refman-html/language/core/variants.html /usr/share/doc/rocq/refman-html/language/extensions /usr/share/doc/rocq/refman-html/language/extensions/arguments-command.html /usr/share/doc/rocq/refman-html/language/extensions/canonical.html /usr/share/doc/rocq/refman-html/language/extensions/compil-steps.html /usr/share/doc/rocq/refman-html/language/extensions/evars.html /usr/share/doc/rocq/refman-html/language/extensions/implicit-arguments.html /usr/share/doc/rocq/refman-html/language/extensions/index.html /usr/share/doc/rocq/refman-html/language/extensions/match.html /usr/share/doc/rocq/refman-html/language/gallina-extensions.html /usr/share/doc/rocq/refman-html/language/gallina-specification-language.html /usr/share/doc/rocq/refman-html/language/module-system.html /usr/share/doc/rocq/refman-html/license.html /usr/share/doc/rocq/refman-html/objects.inv /usr/share/doc/rocq/refman-html/practical-tools /usr/share/doc/rocq/refman-html/practical-tools/coq-commands.html /usr/share/doc/rocq/refman-html/practical-tools/coqide.html /usr/share/doc/rocq/refman-html/practical-tools/utilities.html /usr/share/doc/rocq/refman-html/proof-engine /usr/share/doc/rocq/refman-html/proof-engine/ltac.html /usr/share/doc/rocq/refman-html/proof-engine/ltac2.html /usr/share/doc/rocq/refman-html/proof-engine/proof-handling.html /usr/share/doc/rocq/refman-html/proof-engine/ssreflect-proof-language.html /usr/share/doc/rocq/refman-html/proof-engine/tactics.html /usr/share/doc/rocq/refman-html/proof-engine/vernacular-commands.html /usr/share/doc/rocq/refman-html/proofs /usr/share/doc/rocq/refman-html/proofs/automatic-tactics /usr/share/doc/rocq/refman-html/proofs/automatic-tactics/auto.html /usr/share/doc/rocq/refman-html/proofs/automatic-tactics/index.html /usr/share/doc/rocq/refman-html/proofs/automatic-tactics/logic.html /usr/share/doc/rocq/refman-html/proofs/creating-tactics /usr/share/doc/rocq/refman-html/proofs/creating-tactics/index.html /usr/share/doc/rocq/refman-html/proofs/writing-proofs /usr/share/doc/rocq/refman-html/proofs/writing-proofs/equality.html /usr/share/doc/rocq/refman-html/proofs/writing-proofs/index.html /usr/share/doc/rocq/refman-html/proofs/writing-proofs/proof-mode.html /usr/share/doc/rocq/refman-html/proofs/writing-proofs/reasoning-inductives.html /usr/share/doc/rocq/refman-html/proofs/writing-proofs/rewriting.html /usr/share/doc/rocq/refman-html/rocq-attrindex.html /usr/share/doc/rocq/refman-html/rocq-cmdindex.html /usr/share/doc/rocq/refman-html/rocq-exnindex.html /usr/share/doc/rocq/refman-html/rocq-optindex.html /usr/share/doc/rocq/refman-html/rocq-tacindex.html /usr/share/doc/rocq/refman-html/rocq-thmindex.html /usr/share/doc/rocq/refman-html/search.html /usr/share/doc/rocq/refman-html/searchindex.js /usr/share/doc/rocq/refman-html/std-glossindex.html /usr/share/doc/rocq/refman-html/user-extensions /usr/share/doc/rocq/refman-html/user-extensions/proof-schemes.html /usr/share/doc/rocq/refman-html/user-extensions/syntax-extensions.html /usr/share/doc/rocq/refman-html/using /usr/share/doc/rocq/refman-html/using/libraries /usr/share/doc/rocq/refman-html/using/libraries/funind.html /usr/share/doc/rocq/refman-html/using/libraries/index.html /usr/share/doc/rocq/refman-html/using/libraries/writing.html /usr/share/doc/rocq/refman-html/using/tools /usr/share/doc/rocq/refman-html/using/tools/coqdoc.html /usr/share/doc/rocq/refman-html/using/tools/index.html /usr/share/doc/rocq/refman-html/zebibliography.html /usr/share/doc/rocq/refman-pdf /usr/share/doc/rocq/refman-pdf/rocq-9.2-reference-manual.pdf /usr/share/licenses/rocq-doc /usr/share/licenses/rocq-doc/LICENSE
Generated by rpm2html 1.8.1
Fabrice Bellet, Wed Apr 22 23:40:39 2026