From a711ccba2a769bad17bf2e23f5bbb78f146de2a5 Mon Sep 17 00:00:00 2001 From: Laurent Chardon Date: Wed, 18 Feb 2026 08:46:00 -0500 Subject: [PATCH] math/rocq (math/coq): Update to 9.1.1 --- math/rocq/Makefile | 87 + math/rocq/distinfo | 3 + math/rocq/pkg-descr | 10 + math/rocq/pkg-plist | 4319 +++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 4419 insertions(+) create mode 100644 math/rocq/Makefile create mode 100644 math/rocq/distinfo create mode 100644 math/rocq/pkg-descr create mode 100644 math/rocq/pkg-plist diff --git a/math/rocq/Makefile b/math/rocq/Makefile new file mode 100644 index 000000000000..30854b4aab9f --- /dev/null +++ b/math/rocq/Makefile @@ -0,0 +1,87 @@ +PORTNAME= rocq +PORTVERSION= 9.1.1 +DISTVERSIONPREFIX= V +CATEGORIES= math +PKGNAMESUFFIX= ${EMACS_PKGNAMESUFFIX} + +MAINTAINER= laurent.chardon@gmail.com +COMMENT= Theorem prover based on lambda-C +WWW= https://rocq-prover.org + +LICENSE= LGPL21 +LICENSE_FILE= ${WRKSRC}/LICENSE + +BUILD_DEPENDS= ${SA_DIR}/zarith/META:math/ocaml-zarith \ + bash:shells/bash \ + camlp5:devel/ocaml-camlp5 +LIB_DEPENDS= libgmp.so:math/gmp +RUN_DEPENDS= ${SA_DIR}/num/META:math/ocaml-num \ + ${SA_DIR}/zarith/META:math/ocaml-zarith + +USES= emacs gettext-runtime gmake ocaml:dune,findlib,ldconfig python:env shebangfix tex +USE_GITHUB= yes +GH_ACCOUNT= rocq-prover +USE_LDCONFIG= ${PREFIX}/lib/coq +#OCAML_LDLIBS= ${OCAML_SITELIBDIR}/coq-core + +SHEBANG_FILES= tools/*.py + +HAS_CONFIGURE= yes +CONFIGURE_ARGS= -prefix ${PREFIX} \ + -mandir ${PREFIX}/share/man \ + -docdir ${OCAML_DOCSDIR} \ + -bytecode-compiler yes \ + -native-compiler yes + +OCAML_PACKAGES= rocq-runtime coq-core rocq-core +CONFLICTS_INSTALL= coq coq-emacs_* + +OPTIONS_DEFINE= DOCS IDE +OPTIONS_DEFAULT= IDE +OPTIONS_SUB= yes +IDE_DESC= Include desktop environment (rocqide) +IDE_BUILD_DEPENDS= ${SA_DIR}/lablgtk3/META:x11-toolkits/ocaml-lablgtk3 +IDE_LIB_DEPENDS= libfontconfig.so:x11-fonts/fontconfig \ + libfreetype.so:print/freetype2 \ + libharfbuzz.so:print/harfbuzz +IDE_RUN_DEPENDS= ${SA_DIR}/lablgtk3/META:x11-toolkits/ocaml-lablgtk3 +IDE_USES= gnome +IDE_VARS= ocaml_packages+=coqide-server ocaml_packages+=rocqide +IDE_USE= GNOME=cairo,gdkpixbuf,gtk30,gtksourceview3 + +SA_DIR= ${LOCALBASE}/${OCAML_SITELIBDIR} + +pre-build: + @${MAKE_CMD} -C ${WRKSRC} dunestrap + +do-build: + cd ${WRKSRC} && ${SETENV} ${MAKE_ENV} \ + dune build -p rocq-runtime,coq-core,rocq-core + +do-build-IDE-on: + cd ${WRKSRC} && ${SETENV} ${MAKE_ENV} \ + dune build -p rocq-runtime,coq-core,rocq-core,coqide-server,rocqide + +do-install: + cd ${WRKSRC} && ${SETENV} ${MAKE_ENV} \ + dune install --prefix=${PREFIX} --destdir=${STAGEDIR} \ + rocq-runtime coq-core rocq-core + +do-install-IDE-on: + cd ${WRKSRC} && ${SETENV} ${MAKE_ENV} \ + dune install --prefix=${PREFIX} --destdir=${STAGEDIR} \ + rocq-runtime coq-core rocq-core coqide-server rocqide + +post-install: + @(cd ${STAGEDIR}${PREFIX} ; \ + ${FIND} ${OCAML_SITELIBDIR} -type f '(' -name '*.cmxs' -o -name '*_stubs.so' ')' ; \ + ${FIND} bin -type f -not -name '*.byte' ; \ + ) | while read f; \ + do \ + ${STRIP_CMD} ${STAGEDIR}${PREFIX}/$$f ; \ + done + +post-install-IDE-on: + @${MKDIR} -p ${STAGEDIR}${PREFIX}/etc/xdg/coq + +.include diff --git a/math/rocq/distinfo b/math/rocq/distinfo new file mode 100644 index 000000000000..c16e3efc27ea --- /dev/null +++ b/math/rocq/distinfo @@ -0,0 +1,3 @@ +TIMESTAMP = 1770896106 +SHA256 (rocq-prover-rocq-V9.1.1_GH0.tar.gz) = 35cd03fc4193969b1cce01190340e5c129c1ba8f02242a9e6dff4b83be118759 +SIZE (rocq-prover-rocq-V9.1.1_GH0.tar.gz) = 6395021 diff --git a/math/rocq/pkg-descr b/math/rocq/pkg-descr new file mode 100644 index 000000000000..fc193192d64c --- /dev/null +++ b/math/rocq/pkg-descr @@ -0,0 +1,10 @@ +A trustworthy, industrial-strength interactive theorem prover and +dependently-typed programming language for mechanised reasoning in mathematics, +computer science and more. + +The Rocq Prover is an interactive theorem prover, or proof assistant. This +means that it is designed to develop mathematical proofs, and especially to +write formal specifications: programs and proofs that programs comply to their +specifications. An interesting additional feature of Rocq is that it can +automatically extract executable programs from specifications, as either OCaml +or Haskell source code. diff --git a/math/rocq/pkg-plist b/math/rocq/pkg-plist new file mode 100644 index 000000000000..4ccbabde29fc --- /dev/null +++ b/math/rocq/pkg-plist @@ -0,0 +1,4319 @@ +bin/coq-tex +bin/coq_makefile +bin/coqc +bin/coqchk +bin/coqdep +bin/coqdoc +%%IDE%%bin/coqidetop +bin/coqnative +bin/coqpp +bin/coqtop +bin/coqtop.byte +bin/coqwc +bin/coqworkmgr +bin/csdpcert +bin/ocamllibdep +bin/rocq +bin/rocq.byte +bin/rocqchk +%%IDE%%bin/rocqide +bin/votour +lib/coq-core/META +lib/coq-core/dune-package +lib/coq-core/opam +lib/coq/theories/Array/.coq-native/NCorelib_Array_ArrayAxioms.cmi +lib/coq/theories/Array/.coq-native/NCorelib_Array_ArrayAxioms.cmxs +lib/coq/theories/Array/.coq-native/NCorelib_Array_PrimArray.cmi +lib/coq/theories/Array/.coq-native/NCorelib_Array_PrimArray.cmxs +lib/coq/theories/Array/ArrayAxioms.glob +lib/coq/theories/Array/ArrayAxioms.v +lib/coq/theories/Array/ArrayAxioms.vo +lib/coq/theories/Array/ArrayAxioms.vos +lib/coq/theories/Array/PrimArray.glob +lib/coq/theories/Array/PrimArray.v +lib/coq/theories/Array/PrimArray.vo +lib/coq/theories/Array/PrimArray.vos +lib/coq/theories/BinNums/.coq-native/NCorelib_BinNums_IntDef.cmi +lib/coq/theories/BinNums/.coq-native/NCorelib_BinNums_IntDef.cmxs +lib/coq/theories/BinNums/.coq-native/NCorelib_BinNums_NatDef.cmi +lib/coq/theories/BinNums/.coq-native/NCorelib_BinNums_NatDef.cmxs +lib/coq/theories/BinNums/.coq-native/NCorelib_BinNums_PosDef.cmi +lib/coq/theories/BinNums/.coq-native/NCorelib_BinNums_PosDef.cmxs +lib/coq/theories/BinNums/IntDef.glob +lib/coq/theories/BinNums/IntDef.v +lib/coq/theories/BinNums/IntDef.vo +lib/coq/theories/BinNums/IntDef.vos +lib/coq/theories/BinNums/NatDef.glob +lib/coq/theories/BinNums/NatDef.v +lib/coq/theories/BinNums/NatDef.vo +lib/coq/theories/BinNums/NatDef.vos +lib/coq/theories/BinNums/PosDef.glob +lib/coq/theories/BinNums/PosDef.v +lib/coq/theories/BinNums/PosDef.vo +lib/coq/theories/BinNums/PosDef.vos +lib/coq/theories/Classes/.coq-native/NCorelib_Classes_CMorphisms.cmi +lib/coq/theories/Classes/.coq-native/NCorelib_Classes_CMorphisms.cmxs +lib/coq/theories/Classes/.coq-native/NCorelib_Classes_CRelationClasses.cmi +lib/coq/theories/Classes/.coq-native/NCorelib_Classes_CRelationClasses.cmxs +lib/coq/theories/Classes/.coq-native/NCorelib_Classes_Equivalence.cmi +lib/coq/theories/Classes/.coq-native/NCorelib_Classes_Equivalence.cmxs +lib/coq/theories/Classes/.coq-native/NCorelib_Classes_Init.cmi +lib/coq/theories/Classes/.coq-native/NCorelib_Classes_Init.cmxs +lib/coq/theories/Classes/.coq-native/NCorelib_Classes_Morphisms.cmi +lib/coq/theories/Classes/.coq-native/NCorelib_Classes_Morphisms.cmxs +lib/coq/theories/Classes/.coq-native/NCorelib_Classes_Morphisms_Prop.cmi +lib/coq/theories/Classes/.coq-native/NCorelib_Classes_Morphisms_Prop.cmxs +lib/coq/theories/Classes/.coq-native/NCorelib_Classes_RelationClasses.cmi +lib/coq/theories/Classes/.coq-native/NCorelib_Classes_RelationClasses.cmxs +lib/coq/theories/Classes/.coq-native/NCorelib_Classes_SetoidTactics.cmi +lib/coq/theories/Classes/.coq-native/NCorelib_Classes_SetoidTactics.cmxs +lib/coq/theories/Classes/CMorphisms.glob +lib/coq/theories/Classes/CMorphisms.v +lib/coq/theories/Classes/CMorphisms.vo +lib/coq/theories/Classes/CMorphisms.vos +lib/coq/theories/Classes/CRelationClasses.glob +lib/coq/theories/Classes/CRelationClasses.v +lib/coq/theories/Classes/CRelationClasses.vo +lib/coq/theories/Classes/CRelationClasses.vos +lib/coq/theories/Classes/Equivalence.glob +lib/coq/theories/Classes/Equivalence.v +lib/coq/theories/Classes/Equivalence.vo +lib/coq/theories/Classes/Equivalence.vos +lib/coq/theories/Classes/Init.glob +lib/coq/theories/Classes/Init.v +lib/coq/theories/Classes/Init.vo +lib/coq/theories/Classes/Init.vos +lib/coq/theories/Classes/Morphisms.glob +lib/coq/theories/Classes/Morphisms.v +lib/coq/theories/Classes/Morphisms.vo +lib/coq/theories/Classes/Morphisms.vos +lib/coq/theories/Classes/Morphisms_Prop.glob +lib/coq/theories/Classes/Morphisms_Prop.v +lib/coq/theories/Classes/Morphisms_Prop.vo +lib/coq/theories/Classes/Morphisms_Prop.vos +lib/coq/theories/Classes/RelationClasses.glob +lib/coq/theories/Classes/RelationClasses.v +lib/coq/theories/Classes/RelationClasses.vo +lib/coq/theories/Classes/RelationClasses.vos +lib/coq/theories/Classes/SetoidTactics.glob +lib/coq/theories/Classes/SetoidTactics.v +lib/coq/theories/Classes/SetoidTactics.vo +lib/coq/theories/Classes/SetoidTactics.vos +lib/coq/theories/Compat/.coq-native/NCorelib_Compat_Coq818.cmi +lib/coq/theories/Compat/.coq-native/NCorelib_Compat_Coq818.cmxs +lib/coq/theories/Compat/.coq-native/NCorelib_Compat_Coq819.cmi +lib/coq/theories/Compat/.coq-native/NCorelib_Compat_Coq819.cmxs +lib/coq/theories/Compat/.coq-native/NCorelib_Compat_Coq820.cmi +lib/coq/theories/Compat/.coq-native/NCorelib_Compat_Coq820.cmxs +lib/coq/theories/Compat/.coq-native/NCorelib_Compat_Rocq90.cmi +lib/coq/theories/Compat/.coq-native/NCorelib_Compat_Rocq90.cmxs +lib/coq/theories/Compat/Coq818.glob +lib/coq/theories/Compat/Coq818.v +lib/coq/theories/Compat/Coq818.vo +lib/coq/theories/Compat/Coq818.vos +lib/coq/theories/Compat/Coq819.glob +lib/coq/theories/Compat/Coq819.v +lib/coq/theories/Compat/Coq819.vo +lib/coq/theories/Compat/Coq819.vos +lib/coq/theories/Compat/Coq820.glob +lib/coq/theories/Compat/Coq820.v +lib/coq/theories/Compat/Coq820.vo +lib/coq/theories/Compat/Coq820.vos +lib/coq/theories/Compat/Rocq90.glob +lib/coq/theories/Compat/Rocq90.v +lib/coq/theories/Compat/Rocq90.vo +lib/coq/theories/Compat/Rocq90.vos +lib/coq/theories/Floats/.coq-native/NCorelib_Floats_FloatAxioms.cmi +lib/coq/theories/Floats/.coq-native/NCorelib_Floats_FloatAxioms.cmxs +lib/coq/theories/Floats/.coq-native/NCorelib_Floats_FloatClass.cmi +lib/coq/theories/Floats/.coq-native/NCorelib_Floats_FloatClass.cmxs +lib/coq/theories/Floats/.coq-native/NCorelib_Floats_FloatOps.cmi +lib/coq/theories/Floats/.coq-native/NCorelib_Floats_FloatOps.cmxs +lib/coq/theories/Floats/.coq-native/NCorelib_Floats_PrimFloat.cmi +lib/coq/theories/Floats/.coq-native/NCorelib_Floats_PrimFloat.cmxs +lib/coq/theories/Floats/.coq-native/NCorelib_Floats_SpecFloat.cmi +lib/coq/theories/Floats/.coq-native/NCorelib_Floats_SpecFloat.cmxs +lib/coq/theories/Floats/FloatAxioms.glob +lib/coq/theories/Floats/FloatAxioms.v +lib/coq/theories/Floats/FloatAxioms.vo +lib/coq/theories/Floats/FloatAxioms.vos +lib/coq/theories/Floats/FloatClass.glob +lib/coq/theories/Floats/FloatClass.v +lib/coq/theories/Floats/FloatClass.vo +lib/coq/theories/Floats/FloatClass.vos +lib/coq/theories/Floats/FloatOps.glob +lib/coq/theories/Floats/FloatOps.v +lib/coq/theories/Floats/FloatOps.vo +lib/coq/theories/Floats/FloatOps.vos +lib/coq/theories/Floats/PrimFloat.glob +lib/coq/theories/Floats/PrimFloat.v +lib/coq/theories/Floats/PrimFloat.vo +lib/coq/theories/Floats/PrimFloat.vos +lib/coq/theories/Floats/SpecFloat.glob +lib/coq/theories/Floats/SpecFloat.v +lib/coq/theories/Floats/SpecFloat.vo +lib/coq/theories/Floats/SpecFloat.vos +lib/coq/theories/Init/.coq-native/NCorelib_Init_Byte.cmi +lib/coq/theories/Init/.coq-native/NCorelib_Init_Byte.cmxs +lib/coq/theories/Init/.coq-native/NCorelib_Init_Datatypes.cmi +lib/coq/theories/Init/.coq-native/NCorelib_Init_Datatypes.cmxs +lib/coq/theories/Init/.coq-native/NCorelib_Init_Decimal.cmi +lib/coq/theories/Init/.coq-native/NCorelib_Init_Decimal.cmxs +lib/coq/theories/Init/.coq-native/NCorelib_Init_Hexadecimal.cmi +lib/coq/theories/Init/.coq-native/NCorelib_Init_Hexadecimal.cmxs +lib/coq/theories/Init/.coq-native/NCorelib_Init_Logic.cmi +lib/coq/theories/Init/.coq-native/NCorelib_Init_Logic.cmxs +lib/coq/theories/Init/.coq-native/NCorelib_Init_Ltac.cmi +lib/coq/theories/Init/.coq-native/NCorelib_Init_Ltac.cmxs +lib/coq/theories/Init/.coq-native/NCorelib_Init_Nat.cmi +lib/coq/theories/Init/.coq-native/NCorelib_Init_Nat.cmxs +lib/coq/theories/Init/.coq-native/NCorelib_Init_Notations.cmi +lib/coq/theories/Init/.coq-native/NCorelib_Init_Notations.cmxs +lib/coq/theories/Init/.coq-native/NCorelib_Init_Number.cmi +lib/coq/theories/Init/.coq-native/NCorelib_Init_Number.cmxs +lib/coq/theories/Init/.coq-native/NCorelib_Init_Peano.cmi +lib/coq/theories/Init/.coq-native/NCorelib_Init_Peano.cmxs +lib/coq/theories/Init/.coq-native/NCorelib_Init_Prelude.cmi +lib/coq/theories/Init/.coq-native/NCorelib_Init_Prelude.cmxs +lib/coq/theories/Init/.coq-native/NCorelib_Init_Specif.cmi +lib/coq/theories/Init/.coq-native/NCorelib_Init_Specif.cmxs +lib/coq/theories/Init/.coq-native/NCorelib_Init_Sumbool.cmi +lib/coq/theories/Init/.coq-native/NCorelib_Init_Sumbool.cmxs +lib/coq/theories/Init/.coq-native/NCorelib_Init_Tactics.cmi +lib/coq/theories/Init/.coq-native/NCorelib_Init_Tactics.cmxs +lib/coq/theories/Init/.coq-native/NCorelib_Init_Tauto.cmi +lib/coq/theories/Init/.coq-native/NCorelib_Init_Tauto.cmxs +lib/coq/theories/Init/.coq-native/NCorelib_Init_Wf.cmi +lib/coq/theories/Init/.coq-native/NCorelib_Init_Wf.cmxs +lib/coq/theories/Init/Byte.glob +lib/coq/theories/Init/Byte.v +lib/coq/theories/Init/Byte.vo +lib/coq/theories/Init/Byte.vos +lib/coq/theories/Init/Datatypes.glob +lib/coq/theories/Init/Datatypes.v +lib/coq/theories/Init/Datatypes.vo +lib/coq/theories/Init/Datatypes.vos +lib/coq/theories/Init/Decimal.glob +lib/coq/theories/Init/Decimal.v +lib/coq/theories/Init/Decimal.vo +lib/coq/theories/Init/Decimal.vos +lib/coq/theories/Init/Hexadecimal.glob +lib/coq/theories/Init/Hexadecimal.v +lib/coq/theories/Init/Hexadecimal.vo +lib/coq/theories/Init/Hexadecimal.vos +lib/coq/theories/Init/Logic.glob +lib/coq/theories/Init/Logic.v +lib/coq/theories/Init/Logic.vo +lib/coq/theories/Init/Logic.vos +lib/coq/theories/Init/Ltac.glob +lib/coq/theories/Init/Ltac.v +lib/coq/theories/Init/Ltac.vo +lib/coq/theories/Init/Ltac.vos +lib/coq/theories/Init/Nat.glob +lib/coq/theories/Init/Nat.v +lib/coq/theories/Init/Nat.vo +lib/coq/theories/Init/Nat.vos +lib/coq/theories/Init/Notations.glob +lib/coq/theories/Init/Notations.v +lib/coq/theories/Init/Notations.vo +lib/coq/theories/Init/Notations.vos +lib/coq/theories/Init/Number.glob +lib/coq/theories/Init/Number.v +lib/coq/theories/Init/Number.vo +lib/coq/theories/Init/Number.vos +lib/coq/theories/Init/Peano.glob +lib/coq/theories/Init/Peano.v +lib/coq/theories/Init/Peano.vo +lib/coq/theories/Init/Peano.vos +lib/coq/theories/Init/Prelude.glob +lib/coq/theories/Init/Prelude.v +lib/coq/theories/Init/Prelude.vo +lib/coq/theories/Init/Prelude.vos +lib/coq/theories/Init/Specif.glob +lib/coq/theories/Init/Specif.v +lib/coq/theories/Init/Specif.vo +lib/coq/theories/Init/Specif.vos +lib/coq/theories/Init/Sumbool.glob +lib/coq/theories/Init/Sumbool.v +lib/coq/theories/Init/Sumbool.vo +lib/coq/theories/Init/Sumbool.vos +lib/coq/theories/Init/Tactics.glob +lib/coq/theories/Init/Tactics.v +lib/coq/theories/Init/Tactics.vo +lib/coq/theories/Init/Tactics.vos +lib/coq/theories/Init/Tauto.glob +lib/coq/theories/Init/Tauto.v +lib/coq/theories/Init/Tauto.vo +lib/coq/theories/Init/Tauto.vos +lib/coq/theories/Init/Wf.glob +lib/coq/theories/Init/Wf.v +lib/coq/theories/Init/Wf.vo +lib/coq/theories/Init/Wf.vos +lib/coq/theories/Lists/.coq-native/NCorelib_Lists_ListDef.cmi +lib/coq/theories/Lists/.coq-native/NCorelib_Lists_ListDef.cmxs +lib/coq/theories/Lists/ListDef.glob +lib/coq/theories/Lists/ListDef.v +lib/coq/theories/Lists/ListDef.vo +lib/coq/theories/Lists/ListDef.vos +lib/coq/theories/Numbers/.coq-native/NCorelib_Numbers_BinNums.cmi +lib/coq/theories/Numbers/.coq-native/NCorelib_Numbers_BinNums.cmxs +lib/coq/theories/Numbers/BinNums.glob +lib/coq/theories/Numbers/BinNums.v +lib/coq/theories/Numbers/BinNums.vo +lib/coq/theories/Numbers/BinNums.vos +lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCorelib_Numbers_Cyclic_Int63_CarryType.cmi +lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCorelib_Numbers_Cyclic_Int63_CarryType.cmxs +lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCorelib_Numbers_Cyclic_Int63_PrimInt63.cmi +lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCorelib_Numbers_Cyclic_Int63_PrimInt63.cmxs +lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCorelib_Numbers_Cyclic_Int63_Sint63Axioms.cmi +lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCorelib_Numbers_Cyclic_Int63_Sint63Axioms.cmxs +lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCorelib_Numbers_Cyclic_Int63_Uint63Axioms.cmi +lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCorelib_Numbers_Cyclic_Int63_Uint63Axioms.cmxs +lib/coq/theories/Numbers/Cyclic/Int63/CarryType.glob +lib/coq/theories/Numbers/Cyclic/Int63/CarryType.v +lib/coq/theories/Numbers/Cyclic/Int63/CarryType.vo +lib/coq/theories/Numbers/Cyclic/Int63/CarryType.vos +lib/coq/theories/Numbers/Cyclic/Int63/PrimInt63.glob +lib/coq/theories/Numbers/Cyclic/Int63/PrimInt63.v +lib/coq/theories/Numbers/Cyclic/Int63/PrimInt63.vo +lib/coq/theories/Numbers/Cyclic/Int63/PrimInt63.vos +lib/coq/theories/Numbers/Cyclic/Int63/Sint63Axioms.glob +lib/coq/theories/Numbers/Cyclic/Int63/Sint63Axioms.v +lib/coq/theories/Numbers/Cyclic/Int63/Sint63Axioms.vo +lib/coq/theories/Numbers/Cyclic/Int63/Sint63Axioms.vos +lib/coq/theories/Numbers/Cyclic/Int63/Uint63Axioms.glob +lib/coq/theories/Numbers/Cyclic/Int63/Uint63Axioms.v +lib/coq/theories/Numbers/Cyclic/Int63/Uint63Axioms.vo +lib/coq/theories/Numbers/Cyclic/Int63/Uint63Axioms.vos +lib/coq/theories/Program/.coq-native/NCorelib_Program_Basics.cmi +lib/coq/theories/Program/.coq-native/NCorelib_Program_Basics.cmxs +lib/coq/theories/Program/.coq-native/NCorelib_Program_Tactics.cmi +lib/coq/theories/Program/.coq-native/NCorelib_Program_Tactics.cmxs +lib/coq/theories/Program/.coq-native/NCorelib_Program_Utils.cmi +lib/coq/theories/Program/.coq-native/NCorelib_Program_Utils.cmxs +lib/coq/theories/Program/.coq-native/NCorelib_Program_Wf.cmi +lib/coq/theories/Program/.coq-native/NCorelib_Program_Wf.cmxs +lib/coq/theories/Program/Basics.glob +lib/coq/theories/Program/Basics.v +lib/coq/theories/Program/Basics.vo +lib/coq/theories/Program/Basics.vos +lib/coq/theories/Program/Tactics.glob +lib/coq/theories/Program/Tactics.v +lib/coq/theories/Program/Tactics.vo +lib/coq/theories/Program/Tactics.vos +lib/coq/theories/Program/Utils.glob +lib/coq/theories/Program/Utils.v +lib/coq/theories/Program/Utils.vo +lib/coq/theories/Program/Utils.vos +lib/coq/theories/Program/Wf.glob +lib/coq/theories/Program/Wf.v +lib/coq/theories/Program/Wf.vo +lib/coq/theories/Program/Wf.vos +lib/coq/theories/Relations/.coq-native/NCorelib_Relations_Relation_Definitions.cmi +lib/coq/theories/Relations/.coq-native/NCorelib_Relations_Relation_Definitions.cmxs +lib/coq/theories/Relations/Relation_Definitions.glob +lib/coq/theories/Relations/Relation_Definitions.v +lib/coq/theories/Relations/Relation_Definitions.vo +lib/coq/theories/Relations/Relation_Definitions.vos +lib/coq/theories/Setoids/.coq-native/NCorelib_Setoids_Setoid.cmi +lib/coq/theories/Setoids/.coq-native/NCorelib_Setoids_Setoid.cmxs +lib/coq/theories/Setoids/Setoid.glob +lib/coq/theories/Setoids/Setoid.v +lib/coq/theories/Setoids/Setoid.vo +lib/coq/theories/Setoids/Setoid.vos +lib/coq/theories/Strings/.coq-native/NCorelib_Strings_PrimString.cmi +lib/coq/theories/Strings/.coq-native/NCorelib_Strings_PrimString.cmxs +lib/coq/theories/Strings/.coq-native/NCorelib_Strings_PrimStringAxioms.cmi +lib/coq/theories/Strings/.coq-native/NCorelib_Strings_PrimStringAxioms.cmxs +lib/coq/theories/Strings/PrimString.glob +lib/coq/theories/Strings/PrimString.v +lib/coq/theories/Strings/PrimString.vo +lib/coq/theories/Strings/PrimString.vos +lib/coq/theories/Strings/PrimStringAxioms.glob +lib/coq/theories/Strings/PrimStringAxioms.v +lib/coq/theories/Strings/PrimStringAxioms.vo +lib/coq/theories/Strings/PrimStringAxioms.vos +lib/coq/theories/derive/.coq-native/NCorelib_derive_Derive.cmi +lib/coq/theories/derive/.coq-native/NCorelib_derive_Derive.cmxs +lib/coq/theories/derive/Derive.glob +lib/coq/theories/derive/Derive.v +lib/coq/theories/derive/Derive.vo +lib/coq/theories/derive/Derive.vos +lib/coq/theories/extraction/.coq-native/NCorelib_extraction_ExtrHaskellBasic.cmi +lib/coq/theories/extraction/.coq-native/NCorelib_extraction_ExtrHaskellBasic.cmxs +lib/coq/theories/extraction/.coq-native/NCorelib_extraction_ExtrOcamlBasic.cmi +lib/coq/theories/extraction/.coq-native/NCorelib_extraction_ExtrOcamlBasic.cmxs +lib/coq/theories/extraction/.coq-native/NCorelib_extraction_Extraction.cmi +lib/coq/theories/extraction/.coq-native/NCorelib_extraction_Extraction.cmxs +lib/coq/theories/extraction/ExtrHaskellBasic.glob +lib/coq/theories/extraction/ExtrHaskellBasic.v +lib/coq/theories/extraction/ExtrHaskellBasic.vo +lib/coq/theories/extraction/ExtrHaskellBasic.vos +lib/coq/theories/extraction/ExtrOcamlBasic.glob +lib/coq/theories/extraction/ExtrOcamlBasic.v +lib/coq/theories/extraction/ExtrOcamlBasic.vo +lib/coq/theories/extraction/ExtrOcamlBasic.vos +lib/coq/theories/extraction/Extraction.glob +lib/coq/theories/extraction/Extraction.v +lib/coq/theories/extraction/Extraction.vo +lib/coq/theories/extraction/Extraction.vos +lib/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrbool.cmi +lib/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrbool.cmxs +lib/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrclasses.cmi +lib/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrclasses.cmxs +lib/coq/theories/ssr/.coq-native/NCorelib_ssr_ssreflect.cmi +lib/coq/theories/ssr/.coq-native/NCorelib_ssr_ssreflect.cmxs +lib/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrfun.cmi +lib/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrfun.cmxs +lib/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrsetoid.cmi +lib/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrsetoid.cmxs +lib/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrunder.cmi +lib/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrunder.cmxs +lib/coq/theories/ssr/ssrbool.glob +lib/coq/theories/ssr/ssrbool.v +lib/coq/theories/ssr/ssrbool.vo +lib/coq/theories/ssr/ssrbool.vos +lib/coq/theories/ssr/ssrclasses.glob +lib/coq/theories/ssr/ssrclasses.v +lib/coq/theories/ssr/ssrclasses.vo +lib/coq/theories/ssr/ssrclasses.vos +lib/coq/theories/ssr/ssreflect.glob +lib/coq/theories/ssr/ssreflect.v +lib/coq/theories/ssr/ssreflect.vo +lib/coq/theories/ssr/ssreflect.vos +lib/coq/theories/ssr/ssrfun.glob +lib/coq/theories/ssr/ssrfun.v +lib/coq/theories/ssr/ssrfun.vo +lib/coq/theories/ssr/ssrfun.vos +lib/coq/theories/ssr/ssrsetoid.glob +lib/coq/theories/ssr/ssrsetoid.v +lib/coq/theories/ssr/ssrsetoid.vo +lib/coq/theories/ssr/ssrsetoid.vos +lib/coq/theories/ssr/ssrunder.glob +lib/coq/theories/ssr/ssrunder.v +lib/coq/theories/ssr/ssrunder.vo +lib/coq/theories/ssr/ssrunder.vos +lib/coq/theories/ssrmatching/.coq-native/NCorelib_ssrmatching_ssrmatching.cmi +lib/coq/theories/ssrmatching/.coq-native/NCorelib_ssrmatching_ssrmatching.cmxs +lib/coq/theories/ssrmatching/ssrmatching.glob +lib/coq/theories/ssrmatching/ssrmatching.v +lib/coq/theories/ssrmatching/ssrmatching.vo +lib/coq/theories/ssrmatching/ssrmatching.vos +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Array.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Array.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Bool.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Bool.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Char.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Char.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constant.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constant.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constr.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constr.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constructor.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constructor.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Control.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Control.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Env.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Env.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Evar.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Evar.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_FMap.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_FMap.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_FSet.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_FSet.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Float.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Float.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Fresh.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Fresh.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ident.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ident.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ind.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ind.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Init.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Init.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Int.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Int.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Lazy.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Lazy.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_List.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_List.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac1.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac1.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac1CompatNotations.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac1CompatNotations.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac2.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac2.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Message.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Message.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Meta.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Meta.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Notations.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Notations.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Option.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Option.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pattern.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pattern.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Printf.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Printf.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Proj.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Proj.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pstring.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pstring.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_RedFlags.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_RedFlags.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ref.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ref.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Rewrite.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Rewrite.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Std.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Std.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_String.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_String.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_TransparentState.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_TransparentState.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Uint63.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Uint63.cmxs +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Unification.cmi +lib/coq/user-contrib/Ltac2/.coq-native/NLtac2_Unification.cmxs +lib/coq/user-contrib/Ltac2/Array.glob +lib/coq/user-contrib/Ltac2/Array.v +lib/coq/user-contrib/Ltac2/Array.vo +lib/coq/user-contrib/Ltac2/Array.vos +lib/coq/user-contrib/Ltac2/Bool.glob +lib/coq/user-contrib/Ltac2/Bool.v +lib/coq/user-contrib/Ltac2/Bool.vo +lib/coq/user-contrib/Ltac2/Bool.vos +lib/coq/user-contrib/Ltac2/Char.glob +lib/coq/user-contrib/Ltac2/Char.v +lib/coq/user-contrib/Ltac2/Char.vo +lib/coq/user-contrib/Ltac2/Char.vos +lib/coq/user-contrib/Ltac2/Compat/.coq-native/NLtac2_Compat_Coq818.cmi +lib/coq/user-contrib/Ltac2/Compat/.coq-native/NLtac2_Compat_Coq818.cmxs +lib/coq/user-contrib/Ltac2/Compat/.coq-native/NLtac2_Compat_Coq819.cmi +lib/coq/user-contrib/Ltac2/Compat/.coq-native/NLtac2_Compat_Coq819.cmxs +lib/coq/user-contrib/Ltac2/Compat/Coq818.glob +lib/coq/user-contrib/Ltac2/Compat/Coq818.v +lib/coq/user-contrib/Ltac2/Compat/Coq818.vo +lib/coq/user-contrib/Ltac2/Compat/Coq818.vos +lib/coq/user-contrib/Ltac2/Compat/Coq819.glob +lib/coq/user-contrib/Ltac2/Compat/Coq819.v +lib/coq/user-contrib/Ltac2/Compat/Coq819.vo +lib/coq/user-contrib/Ltac2/Compat/Coq819.vos +lib/coq/user-contrib/Ltac2/Constant.glob +lib/coq/user-contrib/Ltac2/Constant.v +lib/coq/user-contrib/Ltac2/Constant.vo +lib/coq/user-contrib/Ltac2/Constant.vos +lib/coq/user-contrib/Ltac2/Constr.glob +lib/coq/user-contrib/Ltac2/Constr.v +lib/coq/user-contrib/Ltac2/Constr.vo +lib/coq/user-contrib/Ltac2/Constr.vos +lib/coq/user-contrib/Ltac2/Constructor.glob +lib/coq/user-contrib/Ltac2/Constructor.v +lib/coq/user-contrib/Ltac2/Constructor.vo +lib/coq/user-contrib/Ltac2/Constructor.vos +lib/coq/user-contrib/Ltac2/Control.glob +lib/coq/user-contrib/Ltac2/Control.v +lib/coq/user-contrib/Ltac2/Control.vo +lib/coq/user-contrib/Ltac2/Control.vos +lib/coq/user-contrib/Ltac2/Env.glob +lib/coq/user-contrib/Ltac2/Env.v +lib/coq/user-contrib/Ltac2/Env.vo +lib/coq/user-contrib/Ltac2/Env.vos +lib/coq/user-contrib/Ltac2/Evar.glob +lib/coq/user-contrib/Ltac2/Evar.v +lib/coq/user-contrib/Ltac2/Evar.vo +lib/coq/user-contrib/Ltac2/Evar.vos +lib/coq/user-contrib/Ltac2/FMap.glob +lib/coq/user-contrib/Ltac2/FMap.v +lib/coq/user-contrib/Ltac2/FMap.vo +lib/coq/user-contrib/Ltac2/FMap.vos +lib/coq/user-contrib/Ltac2/FSet.glob +lib/coq/user-contrib/Ltac2/FSet.v +lib/coq/user-contrib/Ltac2/FSet.vo +lib/coq/user-contrib/Ltac2/FSet.vos +lib/coq/user-contrib/Ltac2/Float.glob +lib/coq/user-contrib/Ltac2/Float.v +lib/coq/user-contrib/Ltac2/Float.vo +lib/coq/user-contrib/Ltac2/Float.vos +lib/coq/user-contrib/Ltac2/Fresh.glob +lib/coq/user-contrib/Ltac2/Fresh.v +lib/coq/user-contrib/Ltac2/Fresh.vo +lib/coq/user-contrib/Ltac2/Fresh.vos +lib/coq/user-contrib/Ltac2/Ident.glob +lib/coq/user-contrib/Ltac2/Ident.v +lib/coq/user-contrib/Ltac2/Ident.vo +lib/coq/user-contrib/Ltac2/Ident.vos +lib/coq/user-contrib/Ltac2/Ind.glob +lib/coq/user-contrib/Ltac2/Ind.v +lib/coq/user-contrib/Ltac2/Ind.vo +lib/coq/user-contrib/Ltac2/Ind.vos +lib/coq/user-contrib/Ltac2/Init.glob +lib/coq/user-contrib/Ltac2/Init.v +lib/coq/user-contrib/Ltac2/Init.vo +lib/coq/user-contrib/Ltac2/Init.vos +lib/coq/user-contrib/Ltac2/Int.glob +lib/coq/user-contrib/Ltac2/Int.v +lib/coq/user-contrib/Ltac2/Int.vo +lib/coq/user-contrib/Ltac2/Int.vos +lib/coq/user-contrib/Ltac2/Lazy.glob +lib/coq/user-contrib/Ltac2/Lazy.v +lib/coq/user-contrib/Ltac2/Lazy.vo +lib/coq/user-contrib/Ltac2/Lazy.vos +lib/coq/user-contrib/Ltac2/List.glob +lib/coq/user-contrib/Ltac2/List.v +lib/coq/user-contrib/Ltac2/List.vo +lib/coq/user-contrib/Ltac2/List.vos +lib/coq/user-contrib/Ltac2/Ltac1.glob +lib/coq/user-contrib/Ltac2/Ltac1.v +lib/coq/user-contrib/Ltac2/Ltac1.vo +lib/coq/user-contrib/Ltac2/Ltac1.vos +lib/coq/user-contrib/Ltac2/Ltac1CompatNotations.glob +lib/coq/user-contrib/Ltac2/Ltac1CompatNotations.v +lib/coq/user-contrib/Ltac2/Ltac1CompatNotations.vo +lib/coq/user-contrib/Ltac2/Ltac1CompatNotations.vos +lib/coq/user-contrib/Ltac2/Ltac2.glob +lib/coq/user-contrib/Ltac2/Ltac2.v +lib/coq/user-contrib/Ltac2/Ltac2.vo +lib/coq/user-contrib/Ltac2/Ltac2.vos +lib/coq/user-contrib/Ltac2/Message.glob +lib/coq/user-contrib/Ltac2/Message.v +lib/coq/user-contrib/Ltac2/Message.vo +lib/coq/user-contrib/Ltac2/Message.vos +lib/coq/user-contrib/Ltac2/Meta.glob +lib/coq/user-contrib/Ltac2/Meta.v +lib/coq/user-contrib/Ltac2/Meta.vo +lib/coq/user-contrib/Ltac2/Meta.vos +lib/coq/user-contrib/Ltac2/Notations.glob +lib/coq/user-contrib/Ltac2/Notations.v +lib/coq/user-contrib/Ltac2/Notations.vo +lib/coq/user-contrib/Ltac2/Notations.vos +lib/coq/user-contrib/Ltac2/Option.glob +lib/coq/user-contrib/Ltac2/Option.v +lib/coq/user-contrib/Ltac2/Option.vo +lib/coq/user-contrib/Ltac2/Option.vos +lib/coq/user-contrib/Ltac2/Pattern.glob +lib/coq/user-contrib/Ltac2/Pattern.v +lib/coq/user-contrib/Ltac2/Pattern.vo +lib/coq/user-contrib/Ltac2/Pattern.vos +lib/coq/user-contrib/Ltac2/Printf.glob +lib/coq/user-contrib/Ltac2/Printf.v +lib/coq/user-contrib/Ltac2/Printf.vo +lib/coq/user-contrib/Ltac2/Printf.vos +lib/coq/user-contrib/Ltac2/Proj.glob +lib/coq/user-contrib/Ltac2/Proj.v +lib/coq/user-contrib/Ltac2/Proj.vo +lib/coq/user-contrib/Ltac2/Proj.vos +lib/coq/user-contrib/Ltac2/Pstring.glob +lib/coq/user-contrib/Ltac2/Pstring.v +lib/coq/user-contrib/Ltac2/Pstring.vo +lib/coq/user-contrib/Ltac2/Pstring.vos +lib/coq/user-contrib/Ltac2/RedFlags.glob +lib/coq/user-contrib/Ltac2/RedFlags.v +lib/coq/user-contrib/Ltac2/RedFlags.vo +lib/coq/user-contrib/Ltac2/RedFlags.vos +lib/coq/user-contrib/Ltac2/Ref.glob +lib/coq/user-contrib/Ltac2/Ref.v +lib/coq/user-contrib/Ltac2/Ref.vo +lib/coq/user-contrib/Ltac2/Ref.vos +lib/coq/user-contrib/Ltac2/Rewrite.glob +lib/coq/user-contrib/Ltac2/Rewrite.v +lib/coq/user-contrib/Ltac2/Rewrite.vo +lib/coq/user-contrib/Ltac2/Rewrite.vos +lib/coq/user-contrib/Ltac2/Std.glob +lib/coq/user-contrib/Ltac2/Std.v +lib/coq/user-contrib/Ltac2/Std.vo +lib/coq/user-contrib/Ltac2/Std.vos +lib/coq/user-contrib/Ltac2/String.glob +lib/coq/user-contrib/Ltac2/String.v +lib/coq/user-contrib/Ltac2/String.vo +lib/coq/user-contrib/Ltac2/String.vos +lib/coq/user-contrib/Ltac2/TransparentState.glob +lib/coq/user-contrib/Ltac2/TransparentState.v +lib/coq/user-contrib/Ltac2/TransparentState.vo +lib/coq/user-contrib/Ltac2/TransparentState.vos +lib/coq/user-contrib/Ltac2/Uint63.glob +lib/coq/user-contrib/Ltac2/Uint63.v +lib/coq/user-contrib/Ltac2/Uint63.vo +lib/coq/user-contrib/Ltac2/Uint63.vos +lib/coq/user-contrib/Ltac2/Unification.glob +lib/coq/user-contrib/Ltac2/Unification.v +lib/coq/user-contrib/Ltac2/Unification.vo +lib/coq/user-contrib/Ltac2/Unification.vos +%%IDE%%lib/coqide-server/META +%%IDE%%lib/coqide-server/core/core.a +%%IDE%%lib/coqide-server/core/core.cma +%%IDE%%lib/coqide-server/core/core.cmxa +%%IDE%%lib/coqide-server/core/core.cmxs +%%IDE%%lib/coqide-server/core/document.cmi +%%IDE%%lib/coqide-server/core/document.cmt +%%IDE%%lib/coqide-server/core/document.cmti +%%IDE%%lib/coqide-server/core/document.cmx +%%IDE%%lib/coqide-server/core/document.ml +%%IDE%%lib/coqide-server/core/document.mli +%%IDE%%lib/coqide-server/dune-package +%%IDE%%lib/coqide-server/opam +%%IDE%%lib/coqide-server/protocol/interface.cmi +%%IDE%%lib/coqide-server/protocol/interface.cmti +%%IDE%%lib/coqide-server/protocol/interface.mli +%%IDE%%lib/coqide-server/protocol/protocol.a +%%IDE%%lib/coqide-server/protocol/protocol.cma +%%IDE%%lib/coqide-server/protocol/protocol.cmxa +%%IDE%%lib/coqide-server/protocol/protocol.cmxs +%%IDE%%lib/coqide-server/protocol/richpp.cmi +%%IDE%%lib/coqide-server/protocol/richpp.cmt +%%IDE%%lib/coqide-server/protocol/richpp.cmti +%%IDE%%lib/coqide-server/protocol/richpp.cmx +%%IDE%%lib/coqide-server/protocol/richpp.ml +%%IDE%%lib/coqide-server/protocol/richpp.mli +%%IDE%%lib/coqide-server/protocol/serialize.cmi +%%IDE%%lib/coqide-server/protocol/serialize.cmt +%%IDE%%lib/coqide-server/protocol/serialize.cmti +%%IDE%%lib/coqide-server/protocol/serialize.cmx +%%IDE%%lib/coqide-server/protocol/serialize.ml +%%IDE%%lib/coqide-server/protocol/serialize.mli +%%IDE%%lib/coqide-server/protocol/xml_lexer.cmi +%%IDE%%lib/coqide-server/protocol/xml_lexer.cmt +%%IDE%%lib/coqide-server/protocol/xml_lexer.cmti +%%IDE%%lib/coqide-server/protocol/xml_lexer.cmx +%%IDE%%lib/coqide-server/protocol/xml_lexer.ml +%%IDE%%lib/coqide-server/protocol/xml_lexer.mli +%%IDE%%lib/coqide-server/protocol/xml_parser.cmi +%%IDE%%lib/coqide-server/protocol/xml_parser.cmt +%%IDE%%lib/coqide-server/protocol/xml_parser.cmti +%%IDE%%lib/coqide-server/protocol/xml_parser.cmx +%%IDE%%lib/coqide-server/protocol/xml_parser.ml +%%IDE%%lib/coqide-server/protocol/xml_parser.mli +%%IDE%%lib/coqide-server/protocol/xml_printer.cmi +%%IDE%%lib/coqide-server/protocol/xml_printer.cmt +%%IDE%%lib/coqide-server/protocol/xml_printer.cmti +%%IDE%%lib/coqide-server/protocol/xml_printer.cmx +%%IDE%%lib/coqide-server/protocol/xml_printer.ml +%%IDE%%lib/coqide-server/protocol/xml_printer.mli +%%IDE%%lib/coqide-server/protocol/xmlprotocol.cmi +%%IDE%%lib/coqide-server/protocol/xmlprotocol.cmt +%%IDE%%lib/coqide-server/protocol/xmlprotocol.cmti +%%IDE%%lib/coqide-server/protocol/xmlprotocol.cmx +%%IDE%%lib/coqide-server/protocol/xmlprotocol.ml +%%IDE%%lib/coqide-server/protocol/xmlprotocol.mli +lib/rocq-core/META +lib/rocq-core/dune-package +lib/rocq-core/opam +lib/rocq-runtime/META +lib/rocq-runtime/boot/boot.a +lib/rocq-runtime/boot/boot.cma +lib/rocq-runtime/boot/boot.cmi +lib/rocq-runtime/boot/boot.cmt +lib/rocq-runtime/boot/boot.cmx +lib/rocq-runtime/boot/boot.cmxa +lib/rocq-runtime/boot/boot.cmxs +lib/rocq-runtime/boot/boot.ml +lib/rocq-runtime/boot/boot__Env.cmi +lib/rocq-runtime/boot/boot__Env.cmt +lib/rocq-runtime/boot/boot__Env.cmti +lib/rocq-runtime/boot/boot__Env.cmx +lib/rocq-runtime/boot/boot__Path.cmi +lib/rocq-runtime/boot/boot__Path.cmt +lib/rocq-runtime/boot/boot__Path.cmti +lib/rocq-runtime/boot/boot__Path.cmx +lib/rocq-runtime/boot/boot__Usage.cmi +lib/rocq-runtime/boot/boot__Usage.cmt +lib/rocq-runtime/boot/boot__Usage.cmti +lib/rocq-runtime/boot/boot__Usage.cmx +lib/rocq-runtime/boot/boot__Util.cmi +lib/rocq-runtime/boot/boot__Util.cmt +lib/rocq-runtime/boot/boot__Util.cmti +lib/rocq-runtime/boot/boot__Util.cmx +lib/rocq-runtime/boot/env.ml +lib/rocq-runtime/boot/env.mli +lib/rocq-runtime/boot/path.ml +lib/rocq-runtime/boot/path.mli +lib/rocq-runtime/boot/usage.ml +lib/rocq-runtime/boot/usage.mli +lib/rocq-runtime/boot/util.ml +lib/rocq-runtime/boot/util.mli +lib/rocq-runtime/checklib/analyze.ml +lib/rocq-runtime/checklib/analyze.mli +lib/rocq-runtime/checklib/checkFlags.ml +lib/rocq-runtime/checklib/checkFlags.mli +lib/rocq-runtime/checklib/checkInductive.ml +lib/rocq-runtime/checklib/checkInductive.mli +lib/rocq-runtime/checklib/checkLibrary.ml +lib/rocq-runtime/checklib/checkLibrary.mli +lib/rocq-runtime/checklib/check_stat.ml +lib/rocq-runtime/checklib/check_stat.mli +lib/rocq-runtime/checklib/coq_checklib.a +lib/rocq-runtime/checklib/coq_checklib.cma +lib/rocq-runtime/checklib/coq_checklib.cmi +lib/rocq-runtime/checklib/coq_checklib.cmt +lib/rocq-runtime/checklib/coq_checklib.cmx +lib/rocq-runtime/checklib/coq_checklib.cmxa +lib/rocq-runtime/checklib/coq_checklib.cmxs +lib/rocq-runtime/checklib/coq_checklib.ml +lib/rocq-runtime/checklib/coq_checklib__Analyze.cmi +lib/rocq-runtime/checklib/coq_checklib__Analyze.cmt +lib/rocq-runtime/checklib/coq_checklib__Analyze.cmti +lib/rocq-runtime/checklib/coq_checklib__Analyze.cmx +lib/rocq-runtime/checklib/coq_checklib__CheckFlags.cmi +lib/rocq-runtime/checklib/coq_checklib__CheckFlags.cmt +lib/rocq-runtime/checklib/coq_checklib__CheckFlags.cmti +lib/rocq-runtime/checklib/coq_checklib__CheckFlags.cmx +lib/rocq-runtime/checklib/coq_checklib__CheckInductive.cmi +lib/rocq-runtime/checklib/coq_checklib__CheckInductive.cmt +lib/rocq-runtime/checklib/coq_checklib__CheckInductive.cmti +lib/rocq-runtime/checklib/coq_checklib__CheckInductive.cmx +lib/rocq-runtime/checklib/coq_checklib__CheckLibrary.cmi +lib/rocq-runtime/checklib/coq_checklib__CheckLibrary.cmt +lib/rocq-runtime/checklib/coq_checklib__CheckLibrary.cmti +lib/rocq-runtime/checklib/coq_checklib__CheckLibrary.cmx +lib/rocq-runtime/checklib/coq_checklib__Check_stat.cmi +lib/rocq-runtime/checklib/coq_checklib__Check_stat.cmt +lib/rocq-runtime/checklib/coq_checklib__Check_stat.cmti +lib/rocq-runtime/checklib/coq_checklib__Check_stat.cmx +lib/rocq-runtime/checklib/coq_checklib__Coqchk_main.cmi +lib/rocq-runtime/checklib/coq_checklib__Coqchk_main.cmt +lib/rocq-runtime/checklib/coq_checklib__Coqchk_main.cmti +lib/rocq-runtime/checklib/coq_checklib__Coqchk_main.cmx +lib/rocq-runtime/checklib/coq_checklib__Mod_checking.cmi +lib/rocq-runtime/checklib/coq_checklib__Mod_checking.cmt +lib/rocq-runtime/checklib/coq_checklib__Mod_checking.cmti +lib/rocq-runtime/checklib/coq_checklib__Mod_checking.cmx +lib/rocq-runtime/checklib/coq_checklib__Safe_checking.cmi +lib/rocq-runtime/checklib/coq_checklib__Safe_checking.cmt +lib/rocq-runtime/checklib/coq_checklib__Safe_checking.cmti +lib/rocq-runtime/checklib/coq_checklib__Safe_checking.cmx +lib/rocq-runtime/checklib/coq_checklib__Validate.cmi +lib/rocq-runtime/checklib/coq_checklib__Validate.cmt +lib/rocq-runtime/checklib/coq_checklib__Validate.cmti +lib/rocq-runtime/checklib/coq_checklib__Validate.cmx +lib/rocq-runtime/checklib/coq_checklib__Values.cmi +lib/rocq-runtime/checklib/coq_checklib__Values.cmt +lib/rocq-runtime/checklib/coq_checklib__Values.cmti +lib/rocq-runtime/checklib/coq_checklib__Values.cmx +lib/rocq-runtime/checklib/coqchk_main.ml +lib/rocq-runtime/checklib/coqchk_main.mli +lib/rocq-runtime/checklib/mod_checking.ml +lib/rocq-runtime/checklib/mod_checking.mli +lib/rocq-runtime/checklib/safe_checking.ml +lib/rocq-runtime/checklib/safe_checking.mli +lib/rocq-runtime/checklib/validate.ml +lib/rocq-runtime/checklib/validate.mli +lib/rocq-runtime/checklib/values.ml +lib/rocq-runtime/checklib/values.mli +lib/rocq-runtime/clib/cArray.cmi +lib/rocq-runtime/clib/cArray.cmt +lib/rocq-runtime/clib/cArray.cmti +lib/rocq-runtime/clib/cArray.cmx +lib/rocq-runtime/clib/cArray.ml +lib/rocq-runtime/clib/cArray.mli +lib/rocq-runtime/clib/cEphemeron.cmi +lib/rocq-runtime/clib/cEphemeron.cmt +lib/rocq-runtime/clib/cEphemeron.cmti +lib/rocq-runtime/clib/cEphemeron.cmx +lib/rocq-runtime/clib/cEphemeron.ml +lib/rocq-runtime/clib/cEphemeron.mli +lib/rocq-runtime/clib/cList.cmi +lib/rocq-runtime/clib/cList.cmt +lib/rocq-runtime/clib/cList.cmti +lib/rocq-runtime/clib/cList.cmx +lib/rocq-runtime/clib/cList.ml +lib/rocq-runtime/clib/cList.mli +lib/rocq-runtime/clib/cMap.cmi +lib/rocq-runtime/clib/cMap.cmt +lib/rocq-runtime/clib/cMap.cmti +lib/rocq-runtime/clib/cMap.cmx +lib/rocq-runtime/clib/cMap.ml +lib/rocq-runtime/clib/cMap.mli +lib/rocq-runtime/clib/cObj.cmi +lib/rocq-runtime/clib/cObj.cmt +lib/rocq-runtime/clib/cObj.cmti +lib/rocq-runtime/clib/cObj.cmx +lib/rocq-runtime/clib/cObj.ml +lib/rocq-runtime/clib/cObj.mli +lib/rocq-runtime/clib/cSet.cmi +lib/rocq-runtime/clib/cSet.cmt +lib/rocq-runtime/clib/cSet.cmti +lib/rocq-runtime/clib/cSet.cmx +lib/rocq-runtime/clib/cSet.ml +lib/rocq-runtime/clib/cSet.mli +lib/rocq-runtime/clib/cSig.cmi +lib/rocq-runtime/clib/cSig.cmti +lib/rocq-runtime/clib/cSig.mli +lib/rocq-runtime/clib/cString.cmi +lib/rocq-runtime/clib/cString.cmt +lib/rocq-runtime/clib/cString.cmti +lib/rocq-runtime/clib/cString.cmx +lib/rocq-runtime/clib/cString.ml +lib/rocq-runtime/clib/cString.mli +lib/rocq-runtime/clib/cThread.cmi +lib/rocq-runtime/clib/cThread.cmt +lib/rocq-runtime/clib/cThread.cmti +lib/rocq-runtime/clib/cThread.cmx +lib/rocq-runtime/clib/cThread.ml +lib/rocq-runtime/clib/cThread.mli +lib/rocq-runtime/clib/cUnix.cmi +lib/rocq-runtime/clib/cUnix.cmt +lib/rocq-runtime/clib/cUnix.cmti +lib/rocq-runtime/clib/cUnix.cmx +lib/rocq-runtime/clib/cUnix.ml +lib/rocq-runtime/clib/cUnix.mli +lib/rocq-runtime/clib/clib.a +lib/rocq-runtime/clib/clib.cma +lib/rocq-runtime/clib/clib.cmxa +lib/rocq-runtime/clib/clib.cmxs +lib/rocq-runtime/clib/diff2.cmi +lib/rocq-runtime/clib/diff2.cmt +lib/rocq-runtime/clib/diff2.cmti +lib/rocq-runtime/clib/diff2.cmx +lib/rocq-runtime/clib/diff2.ml +lib/rocq-runtime/clib/diff2.mli +lib/rocq-runtime/clib/dyn.cmi +lib/rocq-runtime/clib/dyn.cmt +lib/rocq-runtime/clib/dyn.cmti +lib/rocq-runtime/clib/dyn.cmx +lib/rocq-runtime/clib/dyn.ml +lib/rocq-runtime/clib/dyn.mli +lib/rocq-runtime/clib/exninfo.cmi +lib/rocq-runtime/clib/exninfo.cmt +lib/rocq-runtime/clib/exninfo.cmti +lib/rocq-runtime/clib/exninfo.cmx +lib/rocq-runtime/clib/exninfo.ml +lib/rocq-runtime/clib/exninfo.mli +lib/rocq-runtime/clib/hMap.cmi +lib/rocq-runtime/clib/hMap.cmt +lib/rocq-runtime/clib/hMap.cmti +lib/rocq-runtime/clib/hMap.cmx +lib/rocq-runtime/clib/hMap.ml +lib/rocq-runtime/clib/hMap.mli +lib/rocq-runtime/clib/hashcons.cmi +lib/rocq-runtime/clib/hashcons.cmt +lib/rocq-runtime/clib/hashcons.cmti +lib/rocq-runtime/clib/hashcons.cmx +lib/rocq-runtime/clib/hashcons.ml +lib/rocq-runtime/clib/hashcons.mli +lib/rocq-runtime/clib/hashset.cmi +lib/rocq-runtime/clib/hashset.cmt +lib/rocq-runtime/clib/hashset.cmti +lib/rocq-runtime/clib/hashset.cmx +lib/rocq-runtime/clib/hashset.ml +lib/rocq-runtime/clib/hashset.mli +lib/rocq-runtime/clib/heap.cmi +lib/rocq-runtime/clib/heap.cmt +lib/rocq-runtime/clib/heap.cmti +lib/rocq-runtime/clib/heap.cmx +lib/rocq-runtime/clib/heap.ml +lib/rocq-runtime/clib/heap.mli +lib/rocq-runtime/clib/iStream.cmi +lib/rocq-runtime/clib/iStream.cmt +lib/rocq-runtime/clib/iStream.cmti +lib/rocq-runtime/clib/iStream.cmx +lib/rocq-runtime/clib/iStream.ml +lib/rocq-runtime/clib/iStream.mli +lib/rocq-runtime/clib/int.cmi +lib/rocq-runtime/clib/int.cmt +lib/rocq-runtime/clib/int.cmti +lib/rocq-runtime/clib/int.cmx +lib/rocq-runtime/clib/int.ml +lib/rocq-runtime/clib/int.mli +lib/rocq-runtime/clib/memprof_coq.cmi +lib/rocq-runtime/clib/memprof_coq.cmt +lib/rocq-runtime/clib/memprof_coq.cmti +lib/rocq-runtime/clib/memprof_coq.cmx +lib/rocq-runtime/clib/memprof_coq.ml +lib/rocq-runtime/clib/memprof_coq.mli +lib/rocq-runtime/clib/monad.cmi +lib/rocq-runtime/clib/monad.cmt +lib/rocq-runtime/clib/monad.cmti +lib/rocq-runtime/clib/monad.cmx +lib/rocq-runtime/clib/monad.ml +lib/rocq-runtime/clib/monad.mli +lib/rocq-runtime/clib/mutex_aux.cmi +lib/rocq-runtime/clib/mutex_aux.cmt +lib/rocq-runtime/clib/mutex_aux.cmti +lib/rocq-runtime/clib/mutex_aux.cmx +lib/rocq-runtime/clib/mutex_aux.ml +lib/rocq-runtime/clib/mutex_aux.mli +lib/rocq-runtime/clib/neList.cmi +lib/rocq-runtime/clib/neList.cmt +lib/rocq-runtime/clib/neList.cmti +lib/rocq-runtime/clib/neList.cmx +lib/rocq-runtime/clib/neList.ml +lib/rocq-runtime/clib/neList.mli +lib/rocq-runtime/clib/option.cmi +lib/rocq-runtime/clib/option.cmt +lib/rocq-runtime/clib/option.cmti +lib/rocq-runtime/clib/option.cmx +lib/rocq-runtime/clib/option.ml +lib/rocq-runtime/clib/option.mli +lib/rocq-runtime/clib/orderedType.cmi +lib/rocq-runtime/clib/orderedType.cmt +lib/rocq-runtime/clib/orderedType.cmti +lib/rocq-runtime/clib/orderedType.cmx +lib/rocq-runtime/clib/orderedType.ml +lib/rocq-runtime/clib/orderedType.mli +lib/rocq-runtime/clib/polyMap.cmi +lib/rocq-runtime/clib/polyMap.cmt +lib/rocq-runtime/clib/polyMap.cmti +lib/rocq-runtime/clib/polyMap.cmx +lib/rocq-runtime/clib/polyMap.ml +lib/rocq-runtime/clib/polyMap.mli +lib/rocq-runtime/clib/predicate.cmi +lib/rocq-runtime/clib/predicate.cmt +lib/rocq-runtime/clib/predicate.cmti +lib/rocq-runtime/clib/predicate.cmx +lib/rocq-runtime/clib/predicate.ml +lib/rocq-runtime/clib/predicate.mli +lib/rocq-runtime/clib/range.cmi +lib/rocq-runtime/clib/range.cmt +lib/rocq-runtime/clib/range.cmti +lib/rocq-runtime/clib/range.cmx +lib/rocq-runtime/clib/range.ml +lib/rocq-runtime/clib/range.mli +lib/rocq-runtime/clib/sList.cmi +lib/rocq-runtime/clib/sList.cmt +lib/rocq-runtime/clib/sList.cmti +lib/rocq-runtime/clib/sList.cmx +lib/rocq-runtime/clib/sList.ml +lib/rocq-runtime/clib/sList.mli +lib/rocq-runtime/clib/segmenttree.cmi +lib/rocq-runtime/clib/segmenttree.cmt +lib/rocq-runtime/clib/segmenttree.cmti +lib/rocq-runtime/clib/segmenttree.cmx +lib/rocq-runtime/clib/segmenttree.ml +lib/rocq-runtime/clib/segmenttree.mli +lib/rocq-runtime/clib/store.cmi +lib/rocq-runtime/clib/store.cmt +lib/rocq-runtime/clib/store.cmti +lib/rocq-runtime/clib/store.cmx +lib/rocq-runtime/clib/store.ml +lib/rocq-runtime/clib/store.mli +lib/rocq-runtime/clib/terminal.cmi +lib/rocq-runtime/clib/terminal.cmt +lib/rocq-runtime/clib/terminal.cmti +lib/rocq-runtime/clib/terminal.cmx +lib/rocq-runtime/clib/terminal.ml +lib/rocq-runtime/clib/terminal.mli +lib/rocq-runtime/clib/trie.cmi +lib/rocq-runtime/clib/trie.cmt +lib/rocq-runtime/clib/trie.cmti +lib/rocq-runtime/clib/trie.cmx +lib/rocq-runtime/clib/trie.ml +lib/rocq-runtime/clib/trie.mli +lib/rocq-runtime/clib/unicode.cmi +lib/rocq-runtime/clib/unicode.cmt +lib/rocq-runtime/clib/unicode.cmti +lib/rocq-runtime/clib/unicode.cmx +lib/rocq-runtime/clib/unicode.ml +lib/rocq-runtime/clib/unicode.mli +lib/rocq-runtime/clib/unicodetable.cmi +lib/rocq-runtime/clib/unicodetable.cmt +lib/rocq-runtime/clib/unicodetable.cmti +lib/rocq-runtime/clib/unicodetable.cmx +lib/rocq-runtime/clib/unicodetable.ml +lib/rocq-runtime/clib/unicodetable.mli +lib/rocq-runtime/clib/unionfind.cmi +lib/rocq-runtime/clib/unionfind.cmt +lib/rocq-runtime/clib/unionfind.cmti +lib/rocq-runtime/clib/unionfind.cmx +lib/rocq-runtime/clib/unionfind.ml +lib/rocq-runtime/clib/unionfind.mli +lib/rocq-runtime/config/byte/byte_config.cma +lib/rocq-runtime/config/byte/coq_byte_config.cmi +lib/rocq-runtime/config/byte/coq_byte_config.cmt +lib/rocq-runtime/config/byte/coq_byte_config.cmti +lib/rocq-runtime/config/byte/coq_byte_config.ml +lib/rocq-runtime/config/byte/coq_byte_config.mli +lib/rocq-runtime/config/config.a +lib/rocq-runtime/config/config.cma +lib/rocq-runtime/config/config.cmxa +lib/rocq-runtime/config/config.cmxs +lib/rocq-runtime/config/coq_config.cmi +lib/rocq-runtime/config/coq_config.cmt +lib/rocq-runtime/config/coq_config.cmti +lib/rocq-runtime/config/coq_config.cmx +lib/rocq-runtime/config/coq_config.ml +lib/rocq-runtime/config/coq_config.mli +lib/rocq-runtime/coqargs/coqargs.a +lib/rocq-runtime/coqargs/coqargs.cma +lib/rocq-runtime/coqargs/coqargs.cmi +lib/rocq-runtime/coqargs/coqargs.cmt +lib/rocq-runtime/coqargs/coqargs.cmti +lib/rocq-runtime/coqargs/coqargs.cmx +lib/rocq-runtime/coqargs/coqargs.cmxa +lib/rocq-runtime/coqargs/coqargs.cmxs +lib/rocq-runtime/coqargs/coqargs.ml +lib/rocq-runtime/coqargs/coqargs.mli +lib/rocq-runtime/coqdeplib/args.ml +lib/rocq-runtime/coqdeplib/args.mli +lib/rocq-runtime/coqdeplib/common.ml +lib/rocq-runtime/coqdeplib/common.mli +lib/rocq-runtime/coqdeplib/coqdeplib.a +lib/rocq-runtime/coqdeplib/coqdeplib.cma +lib/rocq-runtime/coqdeplib/coqdeplib.cmi +lib/rocq-runtime/coqdeplib/coqdeplib.cmt +lib/rocq-runtime/coqdeplib/coqdeplib.cmx +lib/rocq-runtime/coqdeplib/coqdeplib.cmxa +lib/rocq-runtime/coqdeplib/coqdeplib.cmxs +lib/rocq-runtime/coqdeplib/coqdeplib.ml +lib/rocq-runtime/coqdeplib/coqdeplib__Args.cmi +lib/rocq-runtime/coqdeplib/coqdeplib__Args.cmt +lib/rocq-runtime/coqdeplib/coqdeplib__Args.cmti +lib/rocq-runtime/coqdeplib/coqdeplib__Args.cmx +lib/rocq-runtime/coqdeplib/coqdeplib__Common.cmi +lib/rocq-runtime/coqdeplib/coqdeplib__Common.cmt +lib/rocq-runtime/coqdeplib/coqdeplib__Common.cmti +lib/rocq-runtime/coqdeplib/coqdeplib__Common.cmx +lib/rocq-runtime/coqdeplib/coqdeplib__Dep_info.cmi +lib/rocq-runtime/coqdeplib/coqdeplib__Dep_info.cmt +lib/rocq-runtime/coqdeplib/coqdeplib__Dep_info.cmti +lib/rocq-runtime/coqdeplib/coqdeplib__Dep_info.cmx +lib/rocq-runtime/coqdeplib/coqdeplib__Error.cmi +lib/rocq-runtime/coqdeplib/coqdeplib__Error.cmt +lib/rocq-runtime/coqdeplib/coqdeplib__Error.cmti +lib/rocq-runtime/coqdeplib/coqdeplib__Error.cmx +lib/rocq-runtime/coqdeplib/coqdeplib__File_util.cmi +lib/rocq-runtime/coqdeplib/coqdeplib__File_util.cmt +lib/rocq-runtime/coqdeplib/coqdeplib__File_util.cmti +lib/rocq-runtime/coqdeplib/coqdeplib__File_util.cmx +lib/rocq-runtime/coqdeplib/coqdeplib__Fl.cmi +lib/rocq-runtime/coqdeplib/coqdeplib__Fl.cmt +lib/rocq-runtime/coqdeplib/coqdeplib__Fl.cmti +lib/rocq-runtime/coqdeplib/coqdeplib__Fl.cmx +lib/rocq-runtime/coqdeplib/coqdeplib__Lexer.cmi +lib/rocq-runtime/coqdeplib/coqdeplib__Lexer.cmt +lib/rocq-runtime/coqdeplib/coqdeplib__Lexer.cmti +lib/rocq-runtime/coqdeplib/coqdeplib__Lexer.cmx +lib/rocq-runtime/coqdeplib/coqdeplib__Loadpath.cmi +lib/rocq-runtime/coqdeplib/coqdeplib__Loadpath.cmt +lib/rocq-runtime/coqdeplib/coqdeplib__Loadpath.cmti +lib/rocq-runtime/coqdeplib/coqdeplib__Loadpath.cmx +lib/rocq-runtime/coqdeplib/coqdeplib__Makefile.cmi +lib/rocq-runtime/coqdeplib/coqdeplib__Makefile.cmt +lib/rocq-runtime/coqdeplib/coqdeplib__Makefile.cmti +lib/rocq-runtime/coqdeplib/coqdeplib__Makefile.cmx +lib/rocq-runtime/coqdeplib/coqdeplib__Rocqdep_main.cmi +lib/rocq-runtime/coqdeplib/coqdeplib__Rocqdep_main.cmt +lib/rocq-runtime/coqdeplib/coqdeplib__Rocqdep_main.cmti +lib/rocq-runtime/coqdeplib/coqdeplib__Rocqdep_main.cmx +lib/rocq-runtime/coqdeplib/coqdeplib__Static_toplevel_libs.cmi +lib/rocq-runtime/coqdeplib/coqdeplib__Static_toplevel_libs.cmt +lib/rocq-runtime/coqdeplib/coqdeplib__Static_toplevel_libs.cmti +lib/rocq-runtime/coqdeplib/coqdeplib__Static_toplevel_libs.cmx +lib/rocq-runtime/coqdeplib/dep_info.ml +lib/rocq-runtime/coqdeplib/dep_info.mli +lib/rocq-runtime/coqdeplib/error.ml +lib/rocq-runtime/coqdeplib/error.mli +lib/rocq-runtime/coqdeplib/file_util.ml +lib/rocq-runtime/coqdeplib/file_util.mli +lib/rocq-runtime/coqdeplib/fl.ml +lib/rocq-runtime/coqdeplib/fl.mli +lib/rocq-runtime/coqdeplib/lexer.ml +lib/rocq-runtime/coqdeplib/lexer.mli +lib/rocq-runtime/coqdeplib/loadpath.ml +lib/rocq-runtime/coqdeplib/loadpath.mli +lib/rocq-runtime/coqdeplib/makefile.ml +lib/rocq-runtime/coqdeplib/makefile.mli +lib/rocq-runtime/coqdeplib/rocqdep_main.ml +lib/rocq-runtime/coqdeplib/rocqdep_main.mli +lib/rocq-runtime/coqdeplib/static_toplevel_libs.ml +lib/rocq-runtime/coqdeplib/static_toplevel_libs.mli +lib/rocq-runtime/coqworkmgrapi/coqworkmgrApi.a +lib/rocq-runtime/coqworkmgrapi/coqworkmgrApi.cma +lib/rocq-runtime/coqworkmgrapi/coqworkmgrApi.cmi +lib/rocq-runtime/coqworkmgrapi/coqworkmgrApi.cmt +lib/rocq-runtime/coqworkmgrapi/coqworkmgrApi.cmti +lib/rocq-runtime/coqworkmgrapi/coqworkmgrApi.cmx +lib/rocq-runtime/coqworkmgrapi/coqworkmgrApi.cmxa +lib/rocq-runtime/coqworkmgrapi/coqworkmgrApi.cmxs +lib/rocq-runtime/coqworkmgrapi/coqworkmgrApi.ml +lib/rocq-runtime/coqworkmgrapi/coqworkmgrApi.mli +lib/rocq-runtime/debugger_support/debugger_support.a +lib/rocq-runtime/debugger_support/debugger_support.cma +lib/rocq-runtime/debugger_support/debugger_support.cmi +lib/rocq-runtime/debugger_support/debugger_support.cmt +lib/rocq-runtime/debugger_support/debugger_support.cmti +lib/rocq-runtime/debugger_support/debugger_support.cmx +lib/rocq-runtime/debugger_support/debugger_support.cmxa +lib/rocq-runtime/debugger_support/debugger_support.cmxs +lib/rocq-runtime/debugger_support/debugger_support.ml +lib/rocq-runtime/debugger_support/debugger_support.mli +lib/rocq-runtime/dev/dev.a +lib/rocq-runtime/dev/dev.cma +lib/rocq-runtime/dev/dev.cmxa +lib/rocq-runtime/dev/dev.cmxs +lib/rocq-runtime/dev/ml_toplevel/include +lib/rocq-runtime/dev/ml_toplevel/include_directories +lib/rocq-runtime/dev/ml_toplevel/include_printers +lib/rocq-runtime/dev/ml_toplevel/include_utilities +lib/rocq-runtime/dev/top_printers.cmi +lib/rocq-runtime/dev/top_printers.cmt +lib/rocq-runtime/dev/top_printers.cmti +lib/rocq-runtime/dev/top_printers.cmx +lib/rocq-runtime/dev/top_printers.ml +lib/rocq-runtime/dev/top_printers.mli +lib/rocq-runtime/dev/vm_printers.cmi +lib/rocq-runtime/dev/vm_printers.cmt +lib/rocq-runtime/dev/vm_printers.cmti +lib/rocq-runtime/dev/vm_printers.cmx +lib/rocq-runtime/dev/vm_printers.ml +lib/rocq-runtime/dev/vm_printers.mli +lib/rocq-runtime/dune-package +lib/rocq-runtime/engine/eConstr.cmi +lib/rocq-runtime/engine/eConstr.cmt +lib/rocq-runtime/engine/eConstr.cmti +lib/rocq-runtime/engine/eConstr.cmx +lib/rocq-runtime/engine/eConstr.ml +lib/rocq-runtime/engine/eConstr.mli +lib/rocq-runtime/engine/engine.a +lib/rocq-runtime/engine/engine.cma +lib/rocq-runtime/engine/engine.cmxa +lib/rocq-runtime/engine/engine.cmxs +lib/rocq-runtime/engine/evar_kinds.cmi +lib/rocq-runtime/engine/evar_kinds.cmt +lib/rocq-runtime/engine/evar_kinds.cmti +lib/rocq-runtime/engine/evar_kinds.cmx +lib/rocq-runtime/engine/evar_kinds.ml +lib/rocq-runtime/engine/evar_kinds.mli +lib/rocq-runtime/engine/evarutil.cmi +lib/rocq-runtime/engine/evarutil.cmt +lib/rocq-runtime/engine/evarutil.cmti +lib/rocq-runtime/engine/evarutil.cmx +lib/rocq-runtime/engine/evarutil.ml +lib/rocq-runtime/engine/evarutil.mli +lib/rocq-runtime/engine/evd.cmi +lib/rocq-runtime/engine/evd.cmt +lib/rocq-runtime/engine/evd.cmti +lib/rocq-runtime/engine/evd.cmx +lib/rocq-runtime/engine/evd.ml +lib/rocq-runtime/engine/evd.mli +lib/rocq-runtime/engine/ftactic.cmi +lib/rocq-runtime/engine/ftactic.cmt +lib/rocq-runtime/engine/ftactic.cmti +lib/rocq-runtime/engine/ftactic.cmx +lib/rocq-runtime/engine/ftactic.ml +lib/rocq-runtime/engine/ftactic.mli +lib/rocq-runtime/engine/logic_monad.cmi +lib/rocq-runtime/engine/logic_monad.cmt +lib/rocq-runtime/engine/logic_monad.cmti +lib/rocq-runtime/engine/logic_monad.cmx +lib/rocq-runtime/engine/logic_monad.ml +lib/rocq-runtime/engine/logic_monad.mli +lib/rocq-runtime/engine/namegen.cmi +lib/rocq-runtime/engine/namegen.cmt +lib/rocq-runtime/engine/namegen.cmti +lib/rocq-runtime/engine/namegen.cmx +lib/rocq-runtime/engine/namegen.ml +lib/rocq-runtime/engine/namegen.mli +lib/rocq-runtime/engine/nameops.cmi +lib/rocq-runtime/engine/nameops.cmt +lib/rocq-runtime/engine/nameops.cmti +lib/rocq-runtime/engine/nameops.cmx +lib/rocq-runtime/engine/nameops.ml +lib/rocq-runtime/engine/nameops.mli +lib/rocq-runtime/engine/profile_tactic.cmi +lib/rocq-runtime/engine/profile_tactic.cmt +lib/rocq-runtime/engine/profile_tactic.cmti +lib/rocq-runtime/engine/profile_tactic.cmx +lib/rocq-runtime/engine/profile_tactic.ml +lib/rocq-runtime/engine/profile_tactic.mli +lib/rocq-runtime/engine/proofview.cmi +lib/rocq-runtime/engine/proofview.cmt +lib/rocq-runtime/engine/proofview.cmti +lib/rocq-runtime/engine/proofview.cmx +lib/rocq-runtime/engine/proofview.ml +lib/rocq-runtime/engine/proofview.mli +lib/rocq-runtime/engine/proofview_monad.cmi +lib/rocq-runtime/engine/proofview_monad.cmt +lib/rocq-runtime/engine/proofview_monad.cmti +lib/rocq-runtime/engine/proofview_monad.cmx +lib/rocq-runtime/engine/proofview_monad.ml +lib/rocq-runtime/engine/proofview_monad.mli +lib/rocq-runtime/engine/termops.cmi +lib/rocq-runtime/engine/termops.cmt +lib/rocq-runtime/engine/termops.cmti +lib/rocq-runtime/engine/termops.cmx +lib/rocq-runtime/engine/termops.ml +lib/rocq-runtime/engine/termops.mli +lib/rocq-runtime/engine/uState.cmi +lib/rocq-runtime/engine/uState.cmt +lib/rocq-runtime/engine/uState.cmti +lib/rocq-runtime/engine/uState.cmx +lib/rocq-runtime/engine/uState.ml +lib/rocq-runtime/engine/uState.mli +lib/rocq-runtime/engine/univFlex.cmi +lib/rocq-runtime/engine/univFlex.cmt +lib/rocq-runtime/engine/univFlex.cmti +lib/rocq-runtime/engine/univFlex.cmx +lib/rocq-runtime/engine/univFlex.ml +lib/rocq-runtime/engine/univFlex.mli +lib/rocq-runtime/engine/univGen.cmi +lib/rocq-runtime/engine/univGen.cmt +lib/rocq-runtime/engine/univGen.cmti +lib/rocq-runtime/engine/univGen.cmx +lib/rocq-runtime/engine/univGen.ml +lib/rocq-runtime/engine/univGen.mli +lib/rocq-runtime/engine/univMinim.cmi +lib/rocq-runtime/engine/univMinim.cmt +lib/rocq-runtime/engine/univMinim.cmti +lib/rocq-runtime/engine/univMinim.cmx +lib/rocq-runtime/engine/univMinim.ml +lib/rocq-runtime/engine/univMinim.mli +lib/rocq-runtime/engine/univNames.cmi +lib/rocq-runtime/engine/univNames.cmt +lib/rocq-runtime/engine/univNames.cmti +lib/rocq-runtime/engine/univNames.cmx +lib/rocq-runtime/engine/univNames.ml +lib/rocq-runtime/engine/univNames.mli +lib/rocq-runtime/engine/univProblem.cmi +lib/rocq-runtime/engine/univProblem.cmt +lib/rocq-runtime/engine/univProblem.cmti +lib/rocq-runtime/engine/univProblem.cmx +lib/rocq-runtime/engine/univProblem.ml +lib/rocq-runtime/engine/univProblem.mli +lib/rocq-runtime/engine/univSubst.cmi +lib/rocq-runtime/engine/univSubst.cmt +lib/rocq-runtime/engine/univSubst.cmti +lib/rocq-runtime/engine/univSubst.cmx +lib/rocq-runtime/engine/univSubst.ml +lib/rocq-runtime/engine/univSubst.mli +lib/rocq-runtime/gramlib/gramext.ml +lib/rocq-runtime/gramlib/gramext.mli +lib/rocq-runtime/gramlib/gramlib.a +lib/rocq-runtime/gramlib/gramlib.cma +lib/rocq-runtime/gramlib/gramlib.cmi +lib/rocq-runtime/gramlib/gramlib.cmt +lib/rocq-runtime/gramlib/gramlib.cmx +lib/rocq-runtime/gramlib/gramlib.cmxa +lib/rocq-runtime/gramlib/gramlib.cmxs +lib/rocq-runtime/gramlib/gramlib.ml +lib/rocq-runtime/gramlib/gramlib__Gramext.cmi +lib/rocq-runtime/gramlib/gramlib__Gramext.cmt +lib/rocq-runtime/gramlib/gramlib__Gramext.cmti +lib/rocq-runtime/gramlib/gramlib__Gramext.cmx +lib/rocq-runtime/gramlib/gramlib__Grammar.cmi +lib/rocq-runtime/gramlib/gramlib__Grammar.cmt +lib/rocq-runtime/gramlib/gramlib__Grammar.cmti +lib/rocq-runtime/gramlib/gramlib__Grammar.cmx +lib/rocq-runtime/gramlib/gramlib__LStream.cmi +lib/rocq-runtime/gramlib/gramlib__LStream.cmt +lib/rocq-runtime/gramlib/gramlib__LStream.cmti +lib/rocq-runtime/gramlib/gramlib__LStream.cmx +lib/rocq-runtime/gramlib/gramlib__Plexing.cmi +lib/rocq-runtime/gramlib/gramlib__Plexing.cmti +lib/rocq-runtime/gramlib/gramlib__Stream.cmi +lib/rocq-runtime/gramlib/gramlib__Stream.cmt +lib/rocq-runtime/gramlib/gramlib__Stream.cmti +lib/rocq-runtime/gramlib/gramlib__Stream.cmx +lib/rocq-runtime/gramlib/grammar.ml +lib/rocq-runtime/gramlib/grammar.mli +lib/rocq-runtime/gramlib/lStream.ml +lib/rocq-runtime/gramlib/lStream.mli +lib/rocq-runtime/gramlib/plexing.mli +lib/rocq-runtime/gramlib/stream.ml +lib/rocq-runtime/gramlib/stream.mli +lib/rocq-runtime/interp/abbreviation.cmi +lib/rocq-runtime/interp/abbreviation.cmt +lib/rocq-runtime/interp/abbreviation.cmti +lib/rocq-runtime/interp/abbreviation.cmx +lib/rocq-runtime/interp/abbreviation.ml +lib/rocq-runtime/interp/abbreviation.mli +lib/rocq-runtime/interp/constrexpr.cmi +lib/rocq-runtime/interp/constrexpr.cmti +lib/rocq-runtime/interp/constrexpr.mli +lib/rocq-runtime/interp/constrexpr_ops.cmi +lib/rocq-runtime/interp/constrexpr_ops.cmt +lib/rocq-runtime/interp/constrexpr_ops.cmti +lib/rocq-runtime/interp/constrexpr_ops.cmx +lib/rocq-runtime/interp/constrexpr_ops.ml +lib/rocq-runtime/interp/constrexpr_ops.mli +lib/rocq-runtime/interp/constrextern.cmi +lib/rocq-runtime/interp/constrextern.cmt +lib/rocq-runtime/interp/constrextern.cmti +lib/rocq-runtime/interp/constrextern.cmx +lib/rocq-runtime/interp/constrextern.ml +lib/rocq-runtime/interp/constrextern.mli +lib/rocq-runtime/interp/constrintern.cmi +lib/rocq-runtime/interp/constrintern.cmt +lib/rocq-runtime/interp/constrintern.cmti +lib/rocq-runtime/interp/constrintern.cmx +lib/rocq-runtime/interp/constrintern.ml +lib/rocq-runtime/interp/constrintern.mli +lib/rocq-runtime/interp/decls.cmi +lib/rocq-runtime/interp/decls.cmt +lib/rocq-runtime/interp/decls.cmti +lib/rocq-runtime/interp/decls.cmx +lib/rocq-runtime/interp/decls.ml +lib/rocq-runtime/interp/decls.mli +lib/rocq-runtime/interp/dumpglob.cmi +lib/rocq-runtime/interp/dumpglob.cmt +lib/rocq-runtime/interp/dumpglob.cmti +lib/rocq-runtime/interp/dumpglob.cmx +lib/rocq-runtime/interp/dumpglob.ml +lib/rocq-runtime/interp/dumpglob.mli +lib/rocq-runtime/interp/genintern.cmi +lib/rocq-runtime/interp/genintern.cmt +lib/rocq-runtime/interp/genintern.cmti +lib/rocq-runtime/interp/genintern.cmx +lib/rocq-runtime/interp/genintern.ml +lib/rocq-runtime/interp/genintern.mli +lib/rocq-runtime/interp/impargs.cmi +lib/rocq-runtime/interp/impargs.cmt +lib/rocq-runtime/interp/impargs.cmti +lib/rocq-runtime/interp/impargs.cmx +lib/rocq-runtime/interp/impargs.ml +lib/rocq-runtime/interp/impargs.mli +lib/rocq-runtime/interp/implicit_quantifiers.cmi +lib/rocq-runtime/interp/implicit_quantifiers.cmt +lib/rocq-runtime/interp/implicit_quantifiers.cmti +lib/rocq-runtime/interp/implicit_quantifiers.cmx +lib/rocq-runtime/interp/implicit_quantifiers.ml +lib/rocq-runtime/interp/implicit_quantifiers.mli +lib/rocq-runtime/interp/interp.a +lib/rocq-runtime/interp/interp.cma +lib/rocq-runtime/interp/interp.cmxa +lib/rocq-runtime/interp/interp.cmxs +lib/rocq-runtime/interp/modintern.cmi +lib/rocq-runtime/interp/modintern.cmt +lib/rocq-runtime/interp/modintern.cmti +lib/rocq-runtime/interp/modintern.cmx +lib/rocq-runtime/interp/modintern.ml +lib/rocq-runtime/interp/modintern.mli +lib/rocq-runtime/interp/notation.cmi +lib/rocq-runtime/interp/notation.cmt +lib/rocq-runtime/interp/notation.cmti +lib/rocq-runtime/interp/notation.cmx +lib/rocq-runtime/interp/notation.ml +lib/rocq-runtime/interp/notation.mli +lib/rocq-runtime/interp/notation_ops.cmi +lib/rocq-runtime/interp/notation_ops.cmt +lib/rocq-runtime/interp/notation_ops.cmti +lib/rocq-runtime/interp/notation_ops.cmx +lib/rocq-runtime/interp/notation_ops.ml +lib/rocq-runtime/interp/notation_ops.mli +lib/rocq-runtime/interp/notation_term.cmi +lib/rocq-runtime/interp/notation_term.cmti +lib/rocq-runtime/interp/notation_term.mli +lib/rocq-runtime/interp/notationextern.cmi +lib/rocq-runtime/interp/notationextern.cmt +lib/rocq-runtime/interp/notationextern.cmti +lib/rocq-runtime/interp/notationextern.cmx +lib/rocq-runtime/interp/notationextern.ml +lib/rocq-runtime/interp/notationextern.mli +lib/rocq-runtime/interp/numTok.cmi +lib/rocq-runtime/interp/numTok.cmt +lib/rocq-runtime/interp/numTok.cmti +lib/rocq-runtime/interp/numTok.cmx +lib/rocq-runtime/interp/numTok.ml +lib/rocq-runtime/interp/numTok.mli +lib/rocq-runtime/interp/reserve.cmi +lib/rocq-runtime/interp/reserve.cmt +lib/rocq-runtime/interp/reserve.cmti +lib/rocq-runtime/interp/reserve.cmx +lib/rocq-runtime/interp/reserve.ml +lib/rocq-runtime/interp/reserve.mli +lib/rocq-runtime/interp/smartlocate.cmi +lib/rocq-runtime/interp/smartlocate.cmt +lib/rocq-runtime/interp/smartlocate.cmti +lib/rocq-runtime/interp/smartlocate.cmx +lib/rocq-runtime/interp/smartlocate.ml +lib/rocq-runtime/interp/smartlocate.mli +lib/rocq-runtime/kernel/cClosure.cmi +lib/rocq-runtime/kernel/cClosure.cmt +lib/rocq-runtime/kernel/cClosure.cmti +lib/rocq-runtime/kernel/cClosure.cmx +lib/rocq-runtime/kernel/cClosure.ml +lib/rocq-runtime/kernel/cClosure.mli +lib/rocq-runtime/kernel/cPrimitives.cmi +lib/rocq-runtime/kernel/cPrimitives.cmt +lib/rocq-runtime/kernel/cPrimitives.cmti +lib/rocq-runtime/kernel/cPrimitives.cmx +lib/rocq-runtime/kernel/cPrimitives.ml +lib/rocq-runtime/kernel/cPrimitives.mli +lib/rocq-runtime/kernel/constant_typing.cmi +lib/rocq-runtime/kernel/constant_typing.cmt +lib/rocq-runtime/kernel/constant_typing.cmti +lib/rocq-runtime/kernel/constant_typing.cmx +lib/rocq-runtime/kernel/constant_typing.ml +lib/rocq-runtime/kernel/constant_typing.mli +lib/rocq-runtime/kernel/constr.cmi +lib/rocq-runtime/kernel/constr.cmt +lib/rocq-runtime/kernel/constr.cmti +lib/rocq-runtime/kernel/constr.cmx +lib/rocq-runtime/kernel/constr.ml +lib/rocq-runtime/kernel/constr.mli +lib/rocq-runtime/kernel/context.cmi +lib/rocq-runtime/kernel/context.cmt +lib/rocq-runtime/kernel/context.cmti +lib/rocq-runtime/kernel/context.cmx +lib/rocq-runtime/kernel/context.ml +lib/rocq-runtime/kernel/context.mli +lib/rocq-runtime/kernel/conv_oracle.cmi +lib/rocq-runtime/kernel/conv_oracle.cmt +lib/rocq-runtime/kernel/conv_oracle.cmti +lib/rocq-runtime/kernel/conv_oracle.cmx +lib/rocq-runtime/kernel/conv_oracle.ml +lib/rocq-runtime/kernel/conv_oracle.mli +lib/rocq-runtime/kernel/conversion.cmi +lib/rocq-runtime/kernel/conversion.cmt +lib/rocq-runtime/kernel/conversion.cmti +lib/rocq-runtime/kernel/conversion.cmx +lib/rocq-runtime/kernel/conversion.ml +lib/rocq-runtime/kernel/conversion.mli +lib/rocq-runtime/kernel/cooking.cmi +lib/rocq-runtime/kernel/cooking.cmt +lib/rocq-runtime/kernel/cooking.cmti +lib/rocq-runtime/kernel/cooking.cmx +lib/rocq-runtime/kernel/cooking.ml +lib/rocq-runtime/kernel/cooking.mli +lib/rocq-runtime/kernel/declarations.cmi +lib/rocq-runtime/kernel/declarations.cmti +lib/rocq-runtime/kernel/declarations.mli +lib/rocq-runtime/kernel/declareops.cmi +lib/rocq-runtime/kernel/declareops.cmt +lib/rocq-runtime/kernel/declareops.cmti +lib/rocq-runtime/kernel/declareops.cmx +lib/rocq-runtime/kernel/declareops.ml +lib/rocq-runtime/kernel/declareops.mli +lib/rocq-runtime/kernel/discharge.cmi +lib/rocq-runtime/kernel/discharge.cmt +lib/rocq-runtime/kernel/discharge.cmti +lib/rocq-runtime/kernel/discharge.cmx +lib/rocq-runtime/kernel/discharge.ml +lib/rocq-runtime/kernel/discharge.mli +lib/rocq-runtime/kernel/entries.cmi +lib/rocq-runtime/kernel/entries.cmti +lib/rocq-runtime/kernel/entries.mli +lib/rocq-runtime/kernel/environ.cmi +lib/rocq-runtime/kernel/environ.cmt +lib/rocq-runtime/kernel/environ.cmti +lib/rocq-runtime/kernel/environ.cmx +lib/rocq-runtime/kernel/environ.ml +lib/rocq-runtime/kernel/environ.mli +lib/rocq-runtime/kernel/esubst.cmi +lib/rocq-runtime/kernel/esubst.cmt +lib/rocq-runtime/kernel/esubst.cmti +lib/rocq-runtime/kernel/esubst.cmx +lib/rocq-runtime/kernel/esubst.ml +lib/rocq-runtime/kernel/esubst.mli +lib/rocq-runtime/kernel/evar.cmi +lib/rocq-runtime/kernel/evar.cmt +lib/rocq-runtime/kernel/evar.cmti +lib/rocq-runtime/kernel/evar.cmx +lib/rocq-runtime/kernel/evar.ml +lib/rocq-runtime/kernel/evar.mli +lib/rocq-runtime/kernel/float64.cmi +lib/rocq-runtime/kernel/float64.cmt +lib/rocq-runtime/kernel/float64.cmti +lib/rocq-runtime/kernel/float64.cmx +lib/rocq-runtime/kernel/float64.ml +lib/rocq-runtime/kernel/float64.mli +lib/rocq-runtime/kernel/float64_common.cmi +lib/rocq-runtime/kernel/float64_common.cmt +lib/rocq-runtime/kernel/float64_common.cmti +lib/rocq-runtime/kernel/float64_common.cmx +lib/rocq-runtime/kernel/float64_common.ml +lib/rocq-runtime/kernel/float64_common.mli +lib/rocq-runtime/kernel/genlambda.cmi +lib/rocq-runtime/kernel/genlambda.cmt +lib/rocq-runtime/kernel/genlambda.cmti +lib/rocq-runtime/kernel/genlambda.cmx +lib/rocq-runtime/kernel/genlambda.ml +lib/rocq-runtime/kernel/genlambda.mli +lib/rocq-runtime/kernel/hConstr.cmi +lib/rocq-runtime/kernel/hConstr.cmt +lib/rocq-runtime/kernel/hConstr.cmti +lib/rocq-runtime/kernel/hConstr.cmx +lib/rocq-runtime/kernel/hConstr.ml +lib/rocq-runtime/kernel/hConstr.mli +lib/rocq-runtime/kernel/indTyping.cmi +lib/rocq-runtime/kernel/indTyping.cmt +lib/rocq-runtime/kernel/indTyping.cmti +lib/rocq-runtime/kernel/indTyping.cmx +lib/rocq-runtime/kernel/indTyping.ml +lib/rocq-runtime/kernel/indTyping.mli +lib/rocq-runtime/kernel/indtypes.cmi +lib/rocq-runtime/kernel/indtypes.cmt +lib/rocq-runtime/kernel/indtypes.cmti +lib/rocq-runtime/kernel/indtypes.cmx +lib/rocq-runtime/kernel/indtypes.ml +lib/rocq-runtime/kernel/indtypes.mli +lib/rocq-runtime/kernel/inductive.cmi +lib/rocq-runtime/kernel/inductive.cmt +lib/rocq-runtime/kernel/inductive.cmti +lib/rocq-runtime/kernel/inductive.cmx +lib/rocq-runtime/kernel/inductive.ml +lib/rocq-runtime/kernel/inductive.mli +lib/rocq-runtime/kernel/inferCumulativity.cmi +lib/rocq-runtime/kernel/inferCumulativity.cmt +lib/rocq-runtime/kernel/inferCumulativity.cmti +lib/rocq-runtime/kernel/inferCumulativity.cmx +lib/rocq-runtime/kernel/inferCumulativity.ml +lib/rocq-runtime/kernel/inferCumulativity.mli +lib/rocq-runtime/kernel/kernel.a +lib/rocq-runtime/kernel/kernel.cma +lib/rocq-runtime/kernel/kernel.cmxa +lib/rocq-runtime/kernel/kernel.cmxs +lib/rocq-runtime/kernel/mod_declarations.cmi +lib/rocq-runtime/kernel/mod_declarations.cmt +lib/rocq-runtime/kernel/mod_declarations.cmti +lib/rocq-runtime/kernel/mod_declarations.cmx +lib/rocq-runtime/kernel/mod_declarations.ml +lib/rocq-runtime/kernel/mod_declarations.mli +lib/rocq-runtime/kernel/mod_subst.cmi +lib/rocq-runtime/kernel/mod_subst.cmt +lib/rocq-runtime/kernel/mod_subst.cmti +lib/rocq-runtime/kernel/mod_subst.cmx +lib/rocq-runtime/kernel/mod_subst.ml +lib/rocq-runtime/kernel/mod_subst.mli +lib/rocq-runtime/kernel/mod_typing.cmi +lib/rocq-runtime/kernel/mod_typing.cmt +lib/rocq-runtime/kernel/mod_typing.cmti +lib/rocq-runtime/kernel/mod_typing.cmx +lib/rocq-runtime/kernel/mod_typing.ml +lib/rocq-runtime/kernel/mod_typing.mli +lib/rocq-runtime/kernel/modops.cmi +lib/rocq-runtime/kernel/modops.cmt +lib/rocq-runtime/kernel/modops.cmti +lib/rocq-runtime/kernel/modops.cmx +lib/rocq-runtime/kernel/modops.ml +lib/rocq-runtime/kernel/modops.mli +lib/rocq-runtime/kernel/names.cmi +lib/rocq-runtime/kernel/names.cmt +lib/rocq-runtime/kernel/names.cmti +lib/rocq-runtime/kernel/names.cmx +lib/rocq-runtime/kernel/names.ml +lib/rocq-runtime/kernel/names.mli +lib/rocq-runtime/kernel/nativecode.cmi +lib/rocq-runtime/kernel/nativecode.cmt +lib/rocq-runtime/kernel/nativecode.cmti +lib/rocq-runtime/kernel/nativecode.cmx +lib/rocq-runtime/kernel/nativecode.ml +lib/rocq-runtime/kernel/nativecode.mli +lib/rocq-runtime/kernel/nativeconv.cmi +lib/rocq-runtime/kernel/nativeconv.cmt +lib/rocq-runtime/kernel/nativeconv.cmti +lib/rocq-runtime/kernel/nativeconv.cmx +lib/rocq-runtime/kernel/nativeconv.ml +lib/rocq-runtime/kernel/nativeconv.mli +lib/rocq-runtime/kernel/nativelambda.cmi +lib/rocq-runtime/kernel/nativelambda.cmt +lib/rocq-runtime/kernel/nativelambda.cmti +lib/rocq-runtime/kernel/nativelambda.cmx +lib/rocq-runtime/kernel/nativelambda.ml +lib/rocq-runtime/kernel/nativelambda.mli +lib/rocq-runtime/kernel/nativelib.cmi +lib/rocq-runtime/kernel/nativelib.cmt +lib/rocq-runtime/kernel/nativelib.cmti +lib/rocq-runtime/kernel/nativelib.cmx +lib/rocq-runtime/kernel/nativelib.ml +lib/rocq-runtime/kernel/nativelib.mli +lib/rocq-runtime/kernel/nativelibrary.cmi +lib/rocq-runtime/kernel/nativelibrary.cmt +lib/rocq-runtime/kernel/nativelibrary.cmti +lib/rocq-runtime/kernel/nativelibrary.cmx +lib/rocq-runtime/kernel/nativelibrary.ml +lib/rocq-runtime/kernel/nativelibrary.mli +lib/rocq-runtime/kernel/nativevalues.cmi +lib/rocq-runtime/kernel/nativevalues.cmt +lib/rocq-runtime/kernel/nativevalues.cmti +lib/rocq-runtime/kernel/nativevalues.cmx +lib/rocq-runtime/kernel/nativevalues.ml +lib/rocq-runtime/kernel/nativevalues.mli +lib/rocq-runtime/kernel/opaqueproof.cmi +lib/rocq-runtime/kernel/opaqueproof.cmt +lib/rocq-runtime/kernel/opaqueproof.cmti +lib/rocq-runtime/kernel/opaqueproof.cmx +lib/rocq-runtime/kernel/opaqueproof.ml +lib/rocq-runtime/kernel/opaqueproof.mli +lib/rocq-runtime/kernel/parray.cmi +lib/rocq-runtime/kernel/parray.cmt +lib/rocq-runtime/kernel/parray.cmti +lib/rocq-runtime/kernel/parray.cmx +lib/rocq-runtime/kernel/parray.ml +lib/rocq-runtime/kernel/parray.mli +lib/rocq-runtime/kernel/partial_subst.cmi +lib/rocq-runtime/kernel/partial_subst.cmt +lib/rocq-runtime/kernel/partial_subst.cmti +lib/rocq-runtime/kernel/partial_subst.cmx +lib/rocq-runtime/kernel/partial_subst.ml +lib/rocq-runtime/kernel/partial_subst.mli +lib/rocq-runtime/kernel/primred.cmi +lib/rocq-runtime/kernel/primred.cmt +lib/rocq-runtime/kernel/primred.cmti +lib/rocq-runtime/kernel/primred.cmx +lib/rocq-runtime/kernel/primred.ml +lib/rocq-runtime/kernel/primred.mli +lib/rocq-runtime/kernel/pstring.cmi +lib/rocq-runtime/kernel/pstring.cmt +lib/rocq-runtime/kernel/pstring.cmti +lib/rocq-runtime/kernel/pstring.cmx +lib/rocq-runtime/kernel/pstring.ml +lib/rocq-runtime/kernel/pstring.mli +lib/rocq-runtime/kernel/redFlags.cmi +lib/rocq-runtime/kernel/redFlags.cmt +lib/rocq-runtime/kernel/redFlags.cmti +lib/rocq-runtime/kernel/redFlags.cmx +lib/rocq-runtime/kernel/redFlags.ml +lib/rocq-runtime/kernel/redFlags.mli +lib/rocq-runtime/kernel/reduction.cmi +lib/rocq-runtime/kernel/reduction.cmt +lib/rocq-runtime/kernel/reduction.cmti +lib/rocq-runtime/kernel/reduction.cmx +lib/rocq-runtime/kernel/reduction.ml +lib/rocq-runtime/kernel/reduction.mli +lib/rocq-runtime/kernel/relevanceops.cmi +lib/rocq-runtime/kernel/relevanceops.cmt +lib/rocq-runtime/kernel/relevanceops.cmti +lib/rocq-runtime/kernel/relevanceops.cmx +lib/rocq-runtime/kernel/relevanceops.ml +lib/rocq-runtime/kernel/relevanceops.mli +lib/rocq-runtime/kernel/retroknowledge.cmi +lib/rocq-runtime/kernel/retroknowledge.cmt +lib/rocq-runtime/kernel/retroknowledge.cmti +lib/rocq-runtime/kernel/retroknowledge.cmx +lib/rocq-runtime/kernel/retroknowledge.ml +lib/rocq-runtime/kernel/retroknowledge.mli +lib/rocq-runtime/kernel/rtree.cmi +lib/rocq-runtime/kernel/rtree.cmt +lib/rocq-runtime/kernel/rtree.cmti +lib/rocq-runtime/kernel/rtree.cmx +lib/rocq-runtime/kernel/rtree.ml +lib/rocq-runtime/kernel/rtree.mli +lib/rocq-runtime/kernel/safe_typing.cmi +lib/rocq-runtime/kernel/safe_typing.cmt +lib/rocq-runtime/kernel/safe_typing.cmti +lib/rocq-runtime/kernel/safe_typing.cmx +lib/rocq-runtime/kernel/safe_typing.ml +lib/rocq-runtime/kernel/safe_typing.mli +lib/rocq-runtime/kernel/section.cmi +lib/rocq-runtime/kernel/section.cmt +lib/rocq-runtime/kernel/section.cmti +lib/rocq-runtime/kernel/section.cmx +lib/rocq-runtime/kernel/section.ml +lib/rocq-runtime/kernel/section.mli +lib/rocq-runtime/kernel/sorts.cmi +lib/rocq-runtime/kernel/sorts.cmt +lib/rocq-runtime/kernel/sorts.cmti +lib/rocq-runtime/kernel/sorts.cmx +lib/rocq-runtime/kernel/sorts.ml +lib/rocq-runtime/kernel/sorts.mli +lib/rocq-runtime/kernel/subtyping.cmi +lib/rocq-runtime/kernel/subtyping.cmt +lib/rocq-runtime/kernel/subtyping.cmti +lib/rocq-runtime/kernel/subtyping.cmx +lib/rocq-runtime/kernel/subtyping.ml +lib/rocq-runtime/kernel/subtyping.mli +lib/rocq-runtime/kernel/term.cmi +lib/rocq-runtime/kernel/term.cmt +lib/rocq-runtime/kernel/term.cmti +lib/rocq-runtime/kernel/term.cmx +lib/rocq-runtime/kernel/term.ml +lib/rocq-runtime/kernel/term.mli +lib/rocq-runtime/kernel/transparentState.cmi +lib/rocq-runtime/kernel/transparentState.cmt +lib/rocq-runtime/kernel/transparentState.cmti +lib/rocq-runtime/kernel/transparentState.cmx +lib/rocq-runtime/kernel/transparentState.ml +lib/rocq-runtime/kernel/transparentState.mli +lib/rocq-runtime/kernel/type_errors.cmi +lib/rocq-runtime/kernel/type_errors.cmt +lib/rocq-runtime/kernel/type_errors.cmti +lib/rocq-runtime/kernel/type_errors.cmx +lib/rocq-runtime/kernel/type_errors.ml +lib/rocq-runtime/kernel/type_errors.mli +lib/rocq-runtime/kernel/typeops.cmi +lib/rocq-runtime/kernel/typeops.cmt +lib/rocq-runtime/kernel/typeops.cmti +lib/rocq-runtime/kernel/typeops.cmx +lib/rocq-runtime/kernel/typeops.ml +lib/rocq-runtime/kernel/typeops.mli +lib/rocq-runtime/kernel/uGraph.cmi +lib/rocq-runtime/kernel/uGraph.cmt +lib/rocq-runtime/kernel/uGraph.cmti +lib/rocq-runtime/kernel/uGraph.cmx +lib/rocq-runtime/kernel/uGraph.ml +lib/rocq-runtime/kernel/uGraph.mli +lib/rocq-runtime/kernel/uVars.cmi +lib/rocq-runtime/kernel/uVars.cmt +lib/rocq-runtime/kernel/uVars.cmti +lib/rocq-runtime/kernel/uVars.cmx +lib/rocq-runtime/kernel/uVars.ml +lib/rocq-runtime/kernel/uVars.mli +lib/rocq-runtime/kernel/uint63.cmi +lib/rocq-runtime/kernel/uint63.cmt +lib/rocq-runtime/kernel/uint63.cmti +lib/rocq-runtime/kernel/uint63.cmx +lib/rocq-runtime/kernel/uint63.ml +lib/rocq-runtime/kernel/uint63.mli +lib/rocq-runtime/kernel/univ.cmi +lib/rocq-runtime/kernel/univ.cmt +lib/rocq-runtime/kernel/univ.cmti +lib/rocq-runtime/kernel/univ.cmx +lib/rocq-runtime/kernel/univ.ml +lib/rocq-runtime/kernel/univ.mli +lib/rocq-runtime/kernel/values.cmi +lib/rocq-runtime/kernel/values.cmti +lib/rocq-runtime/kernel/values.mli +lib/rocq-runtime/kernel/vars.cmi +lib/rocq-runtime/kernel/vars.cmt +lib/rocq-runtime/kernel/vars.cmti +lib/rocq-runtime/kernel/vars.cmx +lib/rocq-runtime/kernel/vars.ml +lib/rocq-runtime/kernel/vars.mli +lib/rocq-runtime/kernel/vconv.cmi +lib/rocq-runtime/kernel/vconv.cmt +lib/rocq-runtime/kernel/vconv.cmti +lib/rocq-runtime/kernel/vconv.cmx +lib/rocq-runtime/kernel/vconv.ml +lib/rocq-runtime/kernel/vconv.mli +lib/rocq-runtime/kernel/vm.cmi +lib/rocq-runtime/kernel/vm.cmt +lib/rocq-runtime/kernel/vm.cmti +lib/rocq-runtime/kernel/vm.cmx +lib/rocq-runtime/kernel/vm.ml +lib/rocq-runtime/kernel/vm.mli +lib/rocq-runtime/kernel/vmbytecodes.cmi +lib/rocq-runtime/kernel/vmbytecodes.cmt +lib/rocq-runtime/kernel/vmbytecodes.cmti +lib/rocq-runtime/kernel/vmbytecodes.cmx +lib/rocq-runtime/kernel/vmbytecodes.ml +lib/rocq-runtime/kernel/vmbytecodes.mli +lib/rocq-runtime/kernel/vmbytegen.cmi +lib/rocq-runtime/kernel/vmbytegen.cmt +lib/rocq-runtime/kernel/vmbytegen.cmti +lib/rocq-runtime/kernel/vmbytegen.cmx +lib/rocq-runtime/kernel/vmbytegen.ml +lib/rocq-runtime/kernel/vmbytegen.mli +lib/rocq-runtime/kernel/vmemitcodes.cmi +lib/rocq-runtime/kernel/vmemitcodes.cmt +lib/rocq-runtime/kernel/vmemitcodes.cmti +lib/rocq-runtime/kernel/vmemitcodes.cmx +lib/rocq-runtime/kernel/vmemitcodes.ml +lib/rocq-runtime/kernel/vmemitcodes.mli +lib/rocq-runtime/kernel/vmerrors.cmi +lib/rocq-runtime/kernel/vmerrors.cmt +lib/rocq-runtime/kernel/vmerrors.cmti +lib/rocq-runtime/kernel/vmerrors.cmx +lib/rocq-runtime/kernel/vmerrors.ml +lib/rocq-runtime/kernel/vmerrors.mli +lib/rocq-runtime/kernel/vmlambda.cmi +lib/rocq-runtime/kernel/vmlambda.cmt +lib/rocq-runtime/kernel/vmlambda.cmti +lib/rocq-runtime/kernel/vmlambda.cmx +lib/rocq-runtime/kernel/vmlambda.ml +lib/rocq-runtime/kernel/vmlambda.mli +lib/rocq-runtime/kernel/vmlibrary.cmi +lib/rocq-runtime/kernel/vmlibrary.cmt +lib/rocq-runtime/kernel/vmlibrary.cmti +lib/rocq-runtime/kernel/vmlibrary.cmx +lib/rocq-runtime/kernel/vmlibrary.ml +lib/rocq-runtime/kernel/vmlibrary.mli +lib/rocq-runtime/kernel/vmopcodes.cmi +lib/rocq-runtime/kernel/vmopcodes.cmt +lib/rocq-runtime/kernel/vmopcodes.cmti +lib/rocq-runtime/kernel/vmopcodes.cmx +lib/rocq-runtime/kernel/vmopcodes.ml +lib/rocq-runtime/kernel/vmopcodes.mli +lib/rocq-runtime/kernel/vmsymtable.cmi +lib/rocq-runtime/kernel/vmsymtable.cmt +lib/rocq-runtime/kernel/vmsymtable.cmti +lib/rocq-runtime/kernel/vmsymtable.cmx +lib/rocq-runtime/kernel/vmsymtable.ml +lib/rocq-runtime/kernel/vmsymtable.mli +lib/rocq-runtime/kernel/vmvalues.cmi +lib/rocq-runtime/kernel/vmvalues.cmt +lib/rocq-runtime/kernel/vmvalues.cmti +lib/rocq-runtime/kernel/vmvalues.cmx +lib/rocq-runtime/kernel/vmvalues.ml +lib/rocq-runtime/kernel/vmvalues.mli +lib/rocq-runtime/lib/acyclicGraph.cmi +lib/rocq-runtime/lib/acyclicGraph.cmt +lib/rocq-runtime/lib/acyclicGraph.cmti +lib/rocq-runtime/lib/acyclicGraph.cmx +lib/rocq-runtime/lib/acyclicGraph.ml +lib/rocq-runtime/lib/acyclicGraph.mli +lib/rocq-runtime/lib/aux_file.cmi +lib/rocq-runtime/lib/aux_file.cmt +lib/rocq-runtime/lib/aux_file.cmti +lib/rocq-runtime/lib/aux_file.cmx +lib/rocq-runtime/lib/aux_file.ml +lib/rocq-runtime/lib/aux_file.mli +lib/rocq-runtime/lib/cAst.cmi +lib/rocq-runtime/lib/cAst.cmt +lib/rocq-runtime/lib/cAst.cmti +lib/rocq-runtime/lib/cAst.cmx +lib/rocq-runtime/lib/cAst.ml +lib/rocq-runtime/lib/cAst.mli +lib/rocq-runtime/lib/cDebug.cmi +lib/rocq-runtime/lib/cDebug.cmt +lib/rocq-runtime/lib/cDebug.cmti +lib/rocq-runtime/lib/cDebug.cmx +lib/rocq-runtime/lib/cDebug.ml +lib/rocq-runtime/lib/cDebug.mli +lib/rocq-runtime/lib/cErrors.cmi +lib/rocq-runtime/lib/cErrors.cmt +lib/rocq-runtime/lib/cErrors.cmti +lib/rocq-runtime/lib/cErrors.cmx +lib/rocq-runtime/lib/cErrors.ml +lib/rocq-runtime/lib/cErrors.mli +lib/rocq-runtime/lib/cWarnings.cmi +lib/rocq-runtime/lib/cWarnings.cmt +lib/rocq-runtime/lib/cWarnings.cmti +lib/rocq-runtime/lib/cWarnings.cmx +lib/rocq-runtime/lib/cWarnings.ml +lib/rocq-runtime/lib/cWarnings.mli +lib/rocq-runtime/lib/control.cmi +lib/rocq-runtime/lib/control.cmt +lib/rocq-runtime/lib/control.cmti +lib/rocq-runtime/lib/control.cmx +lib/rocq-runtime/lib/control.ml +lib/rocq-runtime/lib/control.mli +lib/rocq-runtime/lib/coqProject_file.cmi +lib/rocq-runtime/lib/coqProject_file.cmt +lib/rocq-runtime/lib/coqProject_file.cmti +lib/rocq-runtime/lib/coqProject_file.cmx +lib/rocq-runtime/lib/coqProject_file.ml +lib/rocq-runtime/lib/coqProject_file.mli +lib/rocq-runtime/lib/dAst.cmi +lib/rocq-runtime/lib/dAst.cmt +lib/rocq-runtime/lib/dAst.cmti +lib/rocq-runtime/lib/dAst.cmx +lib/rocq-runtime/lib/dAst.ml +lib/rocq-runtime/lib/dAst.mli +lib/rocq-runtime/lib/deprecation.cmi +lib/rocq-runtime/lib/deprecation.cmt +lib/rocq-runtime/lib/deprecation.cmti +lib/rocq-runtime/lib/deprecation.cmx +lib/rocq-runtime/lib/deprecation.ml +lib/rocq-runtime/lib/deprecation.mli +lib/rocq-runtime/lib/envars.cmi +lib/rocq-runtime/lib/envars.cmt +lib/rocq-runtime/lib/envars.cmti +lib/rocq-runtime/lib/envars.cmx +lib/rocq-runtime/lib/envars.ml +lib/rocq-runtime/lib/envars.mli +lib/rocq-runtime/lib/feedback.cmi +lib/rocq-runtime/lib/feedback.cmt +lib/rocq-runtime/lib/feedback.cmti +lib/rocq-runtime/lib/feedback.cmx +lib/rocq-runtime/lib/feedback.ml +lib/rocq-runtime/lib/feedback.mli +lib/rocq-runtime/lib/flags.cmi +lib/rocq-runtime/lib/flags.cmt +lib/rocq-runtime/lib/flags.cmti +lib/rocq-runtime/lib/flags.cmx +lib/rocq-runtime/lib/flags.ml +lib/rocq-runtime/lib/flags.mli +lib/rocq-runtime/lib/hook.cmi +lib/rocq-runtime/lib/hook.cmt +lib/rocq-runtime/lib/hook.cmti +lib/rocq-runtime/lib/hook.cmx +lib/rocq-runtime/lib/hook.ml +lib/rocq-runtime/lib/hook.mli +lib/rocq-runtime/lib/instr.cmi +lib/rocq-runtime/lib/instr.cmt +lib/rocq-runtime/lib/instr.cmti +lib/rocq-runtime/lib/instr.cmx +lib/rocq-runtime/lib/instr.ml +lib/rocq-runtime/lib/instr.mli +lib/rocq-runtime/lib/lib.a +lib/rocq-runtime/lib/lib.cma +lib/rocq-runtime/lib/lib.cmxa +lib/rocq-runtime/lib/lib.cmxs +lib/rocq-runtime/lib/loc.cmi +lib/rocq-runtime/lib/loc.cmt +lib/rocq-runtime/lib/loc.cmti +lib/rocq-runtime/lib/loc.cmx +lib/rocq-runtime/lib/loc.ml +lib/rocq-runtime/lib/loc.mli +lib/rocq-runtime/lib/newProfile.cmi +lib/rocq-runtime/lib/newProfile.cmt +lib/rocq-runtime/lib/newProfile.cmti +lib/rocq-runtime/lib/newProfile.cmx +lib/rocq-runtime/lib/newProfile.ml +lib/rocq-runtime/lib/newProfile.mli +lib/rocq-runtime/lib/objFile.cmi +lib/rocq-runtime/lib/objFile.cmt +lib/rocq-runtime/lib/objFile.cmti +lib/rocq-runtime/lib/objFile.cmx +lib/rocq-runtime/lib/objFile.ml +lib/rocq-runtime/lib/objFile.mli +lib/rocq-runtime/lib/pp.cmi +lib/rocq-runtime/lib/pp.cmt +lib/rocq-runtime/lib/pp.cmti +lib/rocq-runtime/lib/pp.cmx +lib/rocq-runtime/lib/pp.ml +lib/rocq-runtime/lib/pp.mli +lib/rocq-runtime/lib/pp_diff.cmi +lib/rocq-runtime/lib/pp_diff.cmt +lib/rocq-runtime/lib/pp_diff.cmti +lib/rocq-runtime/lib/pp_diff.cmx +lib/rocq-runtime/lib/pp_diff.ml +lib/rocq-runtime/lib/pp_diff.mli +lib/rocq-runtime/lib/quickfix.cmi +lib/rocq-runtime/lib/quickfix.cmt +lib/rocq-runtime/lib/quickfix.cmti +lib/rocq-runtime/lib/quickfix.cmx +lib/rocq-runtime/lib/quickfix.ml +lib/rocq-runtime/lib/quickfix.mli +lib/rocq-runtime/lib/spawn.cmi +lib/rocq-runtime/lib/spawn.cmt +lib/rocq-runtime/lib/spawn.cmti +lib/rocq-runtime/lib/spawn.cmx +lib/rocq-runtime/lib/spawn.ml +lib/rocq-runtime/lib/spawn.mli +lib/rocq-runtime/lib/stateid.cmi +lib/rocq-runtime/lib/stateid.cmt +lib/rocq-runtime/lib/stateid.cmti +lib/rocq-runtime/lib/stateid.cmx +lib/rocq-runtime/lib/stateid.ml +lib/rocq-runtime/lib/stateid.mli +lib/rocq-runtime/lib/system.cmi +lib/rocq-runtime/lib/system.cmt +lib/rocq-runtime/lib/system.cmti +lib/rocq-runtime/lib/system.cmx +lib/rocq-runtime/lib/system.ml +lib/rocq-runtime/lib/system.mli +lib/rocq-runtime/lib/userWarn.cmi +lib/rocq-runtime/lib/userWarn.cmt +lib/rocq-runtime/lib/userWarn.cmti +lib/rocq-runtime/lib/userWarn.cmx +lib/rocq-runtime/lib/userWarn.ml +lib/rocq-runtime/lib/userWarn.mli +lib/rocq-runtime/lib/util.cmi +lib/rocq-runtime/lib/util.cmt +lib/rocq-runtime/lib/util.cmti +lib/rocq-runtime/lib/util.cmx +lib/rocq-runtime/lib/util.ml +lib/rocq-runtime/lib/util.mli +lib/rocq-runtime/lib/xml_datatype.cmi +lib/rocq-runtime/lib/xml_datatype.cmti +lib/rocq-runtime/lib/xml_datatype.mli +lib/rocq-runtime/library/coqlib.cmi +lib/rocq-runtime/library/coqlib.cmt +lib/rocq-runtime/library/coqlib.cmti +lib/rocq-runtime/library/coqlib.cmx +lib/rocq-runtime/library/coqlib.ml +lib/rocq-runtime/library/coqlib.mli +lib/rocq-runtime/library/global.cmi +lib/rocq-runtime/library/global.cmt +lib/rocq-runtime/library/global.cmti +lib/rocq-runtime/library/global.cmx +lib/rocq-runtime/library/global.ml +lib/rocq-runtime/library/global.mli +lib/rocq-runtime/library/globnames.cmi +lib/rocq-runtime/library/globnames.cmt +lib/rocq-runtime/library/globnames.cmti +lib/rocq-runtime/library/globnames.cmx +lib/rocq-runtime/library/globnames.ml +lib/rocq-runtime/library/globnames.mli +lib/rocq-runtime/library/goptions.cmi +lib/rocq-runtime/library/goptions.cmt +lib/rocq-runtime/library/goptions.cmti +lib/rocq-runtime/library/goptions.cmx +lib/rocq-runtime/library/goptions.ml +lib/rocq-runtime/library/goptions.mli +lib/rocq-runtime/library/lib.cmi +lib/rocq-runtime/library/lib.cmt +lib/rocq-runtime/library/lib.cmti +lib/rocq-runtime/library/lib.cmx +lib/rocq-runtime/library/lib.ml +lib/rocq-runtime/library/lib.mli +lib/rocq-runtime/library/libnames.cmi +lib/rocq-runtime/library/libnames.cmt +lib/rocq-runtime/library/libnames.cmti +lib/rocq-runtime/library/libnames.cmx +lib/rocq-runtime/library/libnames.ml +lib/rocq-runtime/library/libnames.mli +lib/rocq-runtime/library/libobject.cmi +lib/rocq-runtime/library/libobject.cmt +lib/rocq-runtime/library/libobject.cmti +lib/rocq-runtime/library/libobject.cmx +lib/rocq-runtime/library/libobject.ml +lib/rocq-runtime/library/libobject.mli +lib/rocq-runtime/library/library.a +lib/rocq-runtime/library/library.cma +lib/rocq-runtime/library/library.cmxa +lib/rocq-runtime/library/library.cmxs +lib/rocq-runtime/library/library_info.cmi +lib/rocq-runtime/library/library_info.cmt +lib/rocq-runtime/library/library_info.cmti +lib/rocq-runtime/library/library_info.cmx +lib/rocq-runtime/library/library_info.ml +lib/rocq-runtime/library/library_info.mli +lib/rocq-runtime/library/locality.cmi +lib/rocq-runtime/library/locality.cmt +lib/rocq-runtime/library/locality.cmti +lib/rocq-runtime/library/locality.cmx +lib/rocq-runtime/library/locality.ml +lib/rocq-runtime/library/locality.mli +lib/rocq-runtime/library/nametab.cmi +lib/rocq-runtime/library/nametab.cmt +lib/rocq-runtime/library/nametab.cmti +lib/rocq-runtime/library/nametab.cmx +lib/rocq-runtime/library/nametab.ml +lib/rocq-runtime/library/nametab.mli +lib/rocq-runtime/library/rocqlib.cmi +lib/rocq-runtime/library/rocqlib.cmt +lib/rocq-runtime/library/rocqlib.cmti +lib/rocq-runtime/library/rocqlib.cmx +lib/rocq-runtime/library/rocqlib.ml +lib/rocq-runtime/library/rocqlib.mli +lib/rocq-runtime/library/summary.cmi +lib/rocq-runtime/library/summary.cmt +lib/rocq-runtime/library/summary.cmti +lib/rocq-runtime/library/summary.cmx +lib/rocq-runtime/library/summary.ml +lib/rocq-runtime/library/summary.mli +lib/rocq-runtime/opam +lib/rocq-runtime/parsing/cLexer.cmi +lib/rocq-runtime/parsing/cLexer.cmt +lib/rocq-runtime/parsing/cLexer.cmti +lib/rocq-runtime/parsing/cLexer.cmx +lib/rocq-runtime/parsing/cLexer.ml +lib/rocq-runtime/parsing/cLexer.mli +lib/rocq-runtime/parsing/extend.cmi +lib/rocq-runtime/parsing/extend.cmt +lib/rocq-runtime/parsing/extend.cmti +lib/rocq-runtime/parsing/extend.cmx +lib/rocq-runtime/parsing/extend.ml +lib/rocq-runtime/parsing/extend.mli +lib/rocq-runtime/parsing/g_constr.cmi +lib/rocq-runtime/parsing/g_constr.cmt +lib/rocq-runtime/parsing/g_constr.cmti +lib/rocq-runtime/parsing/g_constr.cmx +lib/rocq-runtime/parsing/g_constr.ml +lib/rocq-runtime/parsing/g_constr.mli +lib/rocq-runtime/parsing/g_prim.cmi +lib/rocq-runtime/parsing/g_prim.cmt +lib/rocq-runtime/parsing/g_prim.cmti +lib/rocq-runtime/parsing/g_prim.cmx +lib/rocq-runtime/parsing/g_prim.ml +lib/rocq-runtime/parsing/g_prim.mli +lib/rocq-runtime/parsing/notation_gram.cmi +lib/rocq-runtime/parsing/notation_gram.cmti +lib/rocq-runtime/parsing/notation_gram.mli +lib/rocq-runtime/parsing/notgram_ops.cmi +lib/rocq-runtime/parsing/notgram_ops.cmt +lib/rocq-runtime/parsing/notgram_ops.cmti +lib/rocq-runtime/parsing/notgram_ops.cmx +lib/rocq-runtime/parsing/notgram_ops.ml +lib/rocq-runtime/parsing/notgram_ops.mli +lib/rocq-runtime/parsing/parsing.a +lib/rocq-runtime/parsing/parsing.cma +lib/rocq-runtime/parsing/parsing.cmxa +lib/rocq-runtime/parsing/parsing.cmxs +lib/rocq-runtime/parsing/pcoq.cmi +lib/rocq-runtime/parsing/pcoq.cmt +lib/rocq-runtime/parsing/pcoq.cmti +lib/rocq-runtime/parsing/pcoq.cmx +lib/rocq-runtime/parsing/pcoq.ml +lib/rocq-runtime/parsing/pcoq.mli +lib/rocq-runtime/parsing/procq.cmi +lib/rocq-runtime/parsing/procq.cmt +lib/rocq-runtime/parsing/procq.cmti +lib/rocq-runtime/parsing/procq.cmx +lib/rocq-runtime/parsing/procq.ml +lib/rocq-runtime/parsing/procq.mli +lib/rocq-runtime/parsing/tok.cmi +lib/rocq-runtime/parsing/tok.cmt +lib/rocq-runtime/parsing/tok.cmti +lib/rocq-runtime/parsing/tok.cmx +lib/rocq-runtime/parsing/tok.ml +lib/rocq-runtime/parsing/tok.mli +lib/rocq-runtime/plugins/btauto/btauto_plugin.a +lib/rocq-runtime/plugins/btauto/btauto_plugin.cma +lib/rocq-runtime/plugins/btauto/btauto_plugin.cmi +lib/rocq-runtime/plugins/btauto/btauto_plugin.cmt +lib/rocq-runtime/plugins/btauto/btauto_plugin.cmx +lib/rocq-runtime/plugins/btauto/btauto_plugin.cmxa +lib/rocq-runtime/plugins/btauto/btauto_plugin.cmxs +lib/rocq-runtime/plugins/btauto/btauto_plugin.ml +lib/rocq-runtime/plugins/btauto/btauto_plugin__G_btauto.cmi +lib/rocq-runtime/plugins/btauto/btauto_plugin__G_btauto.cmt +lib/rocq-runtime/plugins/btauto/btauto_plugin__G_btauto.cmti +lib/rocq-runtime/plugins/btauto/btauto_plugin__G_btauto.cmx +lib/rocq-runtime/plugins/btauto/btauto_plugin__Refl_btauto.cmi +lib/rocq-runtime/plugins/btauto/btauto_plugin__Refl_btauto.cmt +lib/rocq-runtime/plugins/btauto/btauto_plugin__Refl_btauto.cmti +lib/rocq-runtime/plugins/btauto/btauto_plugin__Refl_btauto.cmx +lib/rocq-runtime/plugins/btauto/g_btauto.ml +lib/rocq-runtime/plugins/btauto/g_btauto.mli +lib/rocq-runtime/plugins/btauto/refl_btauto.ml +lib/rocq-runtime/plugins/btauto/refl_btauto.mli +lib/rocq-runtime/plugins/cc/cc_plugin.a +lib/rocq-runtime/plugins/cc/cc_plugin.cma +lib/rocq-runtime/plugins/cc/cc_plugin.cmi +lib/rocq-runtime/plugins/cc/cc_plugin.cmt +lib/rocq-runtime/plugins/cc/cc_plugin.cmx +lib/rocq-runtime/plugins/cc/cc_plugin.cmxa +lib/rocq-runtime/plugins/cc/cc_plugin.cmxs +lib/rocq-runtime/plugins/cc/cc_plugin.ml +lib/rocq-runtime/plugins/cc/cc_plugin__G_congruence.cmi +lib/rocq-runtime/plugins/cc/cc_plugin__G_congruence.cmt +lib/rocq-runtime/plugins/cc/cc_plugin__G_congruence.cmti +lib/rocq-runtime/plugins/cc/cc_plugin__G_congruence.cmx +lib/rocq-runtime/plugins/cc/g_congruence.ml +lib/rocq-runtime/plugins/cc/g_congruence.mli +lib/rocq-runtime/plugins/cc_core/cc_core_plugin.a +lib/rocq-runtime/plugins/cc_core/cc_core_plugin.cma +lib/rocq-runtime/plugins/cc_core/cc_core_plugin.cmi +lib/rocq-runtime/plugins/cc_core/cc_core_plugin.cmt +lib/rocq-runtime/plugins/cc_core/cc_core_plugin.cmx +lib/rocq-runtime/plugins/cc_core/cc_core_plugin.cmxa +lib/rocq-runtime/plugins/cc_core/cc_core_plugin.cmxs +lib/rocq-runtime/plugins/cc_core/cc_core_plugin.ml +lib/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccalgo.cmi +lib/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccalgo.cmt +lib/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccalgo.cmti +lib/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccalgo.cmx +lib/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccprojectability.cmi +lib/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccprojectability.cmt +lib/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccprojectability.cmti +lib/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccprojectability.cmx +lib/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccproof.cmi +lib/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccproof.cmt +lib/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccproof.cmti +lib/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccproof.cmx +lib/rocq-runtime/plugins/cc_core/cc_core_plugin__Cctac.cmi +lib/rocq-runtime/plugins/cc_core/cc_core_plugin__Cctac.cmt +lib/rocq-runtime/plugins/cc_core/cc_core_plugin__Cctac.cmti +lib/rocq-runtime/plugins/cc_core/cc_core_plugin__Cctac.cmx +lib/rocq-runtime/plugins/cc_core/ccalgo.ml +lib/rocq-runtime/plugins/cc_core/ccalgo.mli +lib/rocq-runtime/plugins/cc_core/ccprojectability.ml +lib/rocq-runtime/plugins/cc_core/ccprojectability.mli +lib/rocq-runtime/plugins/cc_core/ccproof.ml +lib/rocq-runtime/plugins/cc_core/ccproof.mli +lib/rocq-runtime/plugins/cc_core/cctac.ml +lib/rocq-runtime/plugins/cc_core/cctac.mli +lib/rocq-runtime/plugins/derive/derive.ml +lib/rocq-runtime/plugins/derive/derive.mli +lib/rocq-runtime/plugins/derive/derive_plugin.a +lib/rocq-runtime/plugins/derive/derive_plugin.cma +lib/rocq-runtime/plugins/derive/derive_plugin.cmi +lib/rocq-runtime/plugins/derive/derive_plugin.cmt +lib/rocq-runtime/plugins/derive/derive_plugin.cmx +lib/rocq-runtime/plugins/derive/derive_plugin.cmxa +lib/rocq-runtime/plugins/derive/derive_plugin.cmxs +lib/rocq-runtime/plugins/derive/derive_plugin.ml +lib/rocq-runtime/plugins/derive/derive_plugin__Derive.cmi +lib/rocq-runtime/plugins/derive/derive_plugin__Derive.cmt +lib/rocq-runtime/plugins/derive/derive_plugin__Derive.cmti +lib/rocq-runtime/plugins/derive/derive_plugin__Derive.cmx +lib/rocq-runtime/plugins/derive/derive_plugin__G_derive.cmi +lib/rocq-runtime/plugins/derive/derive_plugin__G_derive.cmt +lib/rocq-runtime/plugins/derive/derive_plugin__G_derive.cmti +lib/rocq-runtime/plugins/derive/derive_plugin__G_derive.cmx +lib/rocq-runtime/plugins/derive/g_derive.ml +lib/rocq-runtime/plugins/derive/g_derive.mli +lib/rocq-runtime/plugins/extraction/common.ml +lib/rocq-runtime/plugins/extraction/common.mli +lib/rocq-runtime/plugins/extraction/extract_env.ml +lib/rocq-runtime/plugins/extraction/extract_env.mli +lib/rocq-runtime/plugins/extraction/extraction.ml +lib/rocq-runtime/plugins/extraction/extraction.mli +lib/rocq-runtime/plugins/extraction/extraction_plugin.a +lib/rocq-runtime/plugins/extraction/extraction_plugin.cma +lib/rocq-runtime/plugins/extraction/extraction_plugin.cmi +lib/rocq-runtime/plugins/extraction/extraction_plugin.cmt +lib/rocq-runtime/plugins/extraction/extraction_plugin.cmx +lib/rocq-runtime/plugins/extraction/extraction_plugin.cmxa +lib/rocq-runtime/plugins/extraction/extraction_plugin.cmxs +lib/rocq-runtime/plugins/extraction/extraction_plugin.ml +lib/rocq-runtime/plugins/extraction/extraction_plugin__Common.cmi +lib/rocq-runtime/plugins/extraction/extraction_plugin__Common.cmt +lib/rocq-runtime/plugins/extraction/extraction_plugin__Common.cmti +lib/rocq-runtime/plugins/extraction/extraction_plugin__Common.cmx +lib/rocq-runtime/plugins/extraction/extraction_plugin__Extract_env.cmi +lib/rocq-runtime/plugins/extraction/extraction_plugin__Extract_env.cmt +lib/rocq-runtime/plugins/extraction/extraction_plugin__Extract_env.cmti +lib/rocq-runtime/plugins/extraction/extraction_plugin__Extract_env.cmx +lib/rocq-runtime/plugins/extraction/extraction_plugin__Extraction.cmi +lib/rocq-runtime/plugins/extraction/extraction_plugin__Extraction.cmt +lib/rocq-runtime/plugins/extraction/extraction_plugin__Extraction.cmti +lib/rocq-runtime/plugins/extraction/extraction_plugin__Extraction.cmx +lib/rocq-runtime/plugins/extraction/extraction_plugin__G_extraction.cmi +lib/rocq-runtime/plugins/extraction/extraction_plugin__G_extraction.cmt +lib/rocq-runtime/plugins/extraction/extraction_plugin__G_extraction.cmti +lib/rocq-runtime/plugins/extraction/extraction_plugin__G_extraction.cmx +lib/rocq-runtime/plugins/extraction/extraction_plugin__Haskell.cmi +lib/rocq-runtime/plugins/extraction/extraction_plugin__Haskell.cmt +lib/rocq-runtime/plugins/extraction/extraction_plugin__Haskell.cmti +lib/rocq-runtime/plugins/extraction/extraction_plugin__Haskell.cmx +lib/rocq-runtime/plugins/extraction/extraction_plugin__Json.cmi +lib/rocq-runtime/plugins/extraction/extraction_plugin__Json.cmt +lib/rocq-runtime/plugins/extraction/extraction_plugin__Json.cmti +lib/rocq-runtime/plugins/extraction/extraction_plugin__Json.cmx +lib/rocq-runtime/plugins/extraction/extraction_plugin__Miniml.cmi +lib/rocq-runtime/plugins/extraction/extraction_plugin__Miniml.cmt +lib/rocq-runtime/plugins/extraction/extraction_plugin__Miniml.cmti +lib/rocq-runtime/plugins/extraction/extraction_plugin__Miniml.cmx +lib/rocq-runtime/plugins/extraction/extraction_plugin__Mlutil.cmi +lib/rocq-runtime/plugins/extraction/extraction_plugin__Mlutil.cmt +lib/rocq-runtime/plugins/extraction/extraction_plugin__Mlutil.cmti +lib/rocq-runtime/plugins/extraction/extraction_plugin__Mlutil.cmx +lib/rocq-runtime/plugins/extraction/extraction_plugin__Modutil.cmi +lib/rocq-runtime/plugins/extraction/extraction_plugin__Modutil.cmt +lib/rocq-runtime/plugins/extraction/extraction_plugin__Modutil.cmti +lib/rocq-runtime/plugins/extraction/extraction_plugin__Modutil.cmx +lib/rocq-runtime/plugins/extraction/extraction_plugin__Ocaml.cmi +lib/rocq-runtime/plugins/extraction/extraction_plugin__Ocaml.cmt +lib/rocq-runtime/plugins/extraction/extraction_plugin__Ocaml.cmti +lib/rocq-runtime/plugins/extraction/extraction_plugin__Ocaml.cmx +lib/rocq-runtime/plugins/extraction/extraction_plugin__Scheme.cmi +lib/rocq-runtime/plugins/extraction/extraction_plugin__Scheme.cmt +lib/rocq-runtime/plugins/extraction/extraction_plugin__Scheme.cmti +lib/rocq-runtime/plugins/extraction/extraction_plugin__Scheme.cmx +lib/rocq-runtime/plugins/extraction/extraction_plugin__Table.cmi +lib/rocq-runtime/plugins/extraction/extraction_plugin__Table.cmt +lib/rocq-runtime/plugins/extraction/extraction_plugin__Table.cmti +lib/rocq-runtime/plugins/extraction/extraction_plugin__Table.cmx +lib/rocq-runtime/plugins/extraction/g_extraction.ml +lib/rocq-runtime/plugins/extraction/g_extraction.mli +lib/rocq-runtime/plugins/extraction/haskell.ml +lib/rocq-runtime/plugins/extraction/haskell.mli +lib/rocq-runtime/plugins/extraction/json.ml +lib/rocq-runtime/plugins/extraction/json.mli +lib/rocq-runtime/plugins/extraction/miniml.ml +lib/rocq-runtime/plugins/extraction/miniml.mli +lib/rocq-runtime/plugins/extraction/mlutil.ml +lib/rocq-runtime/plugins/extraction/mlutil.mli +lib/rocq-runtime/plugins/extraction/modutil.ml +lib/rocq-runtime/plugins/extraction/modutil.mli +lib/rocq-runtime/plugins/extraction/ocaml.ml +lib/rocq-runtime/plugins/extraction/ocaml.mli +lib/rocq-runtime/plugins/extraction/scheme.ml +lib/rocq-runtime/plugins/extraction/scheme.mli +lib/rocq-runtime/plugins/extraction/table.ml +lib/rocq-runtime/plugins/extraction/table.mli +lib/rocq-runtime/plugins/firstorder/firstorder_plugin.a +lib/rocq-runtime/plugins/firstorder/firstorder_plugin.cma +lib/rocq-runtime/plugins/firstorder/firstorder_plugin.cmi +lib/rocq-runtime/plugins/firstorder/firstorder_plugin.cmt +lib/rocq-runtime/plugins/firstorder/firstorder_plugin.cmx +lib/rocq-runtime/plugins/firstorder/firstorder_plugin.cmxa +lib/rocq-runtime/plugins/firstorder/firstorder_plugin.cmxs +lib/rocq-runtime/plugins/firstorder/firstorder_plugin.ml +lib/rocq-runtime/plugins/firstorder/firstorder_plugin__G_ground.cmi +lib/rocq-runtime/plugins/firstorder/firstorder_plugin__G_ground.cmt +lib/rocq-runtime/plugins/firstorder/firstorder_plugin__G_ground.cmti +lib/rocq-runtime/plugins/firstorder/firstorder_plugin__G_ground.cmx +lib/rocq-runtime/plugins/firstorder/g_ground.ml +lib/rocq-runtime/plugins/firstorder/g_ground.mli +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin.a +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin.cma +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin.cmi +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin.cmt +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin.cmx +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin.cmxa +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin.cmxs +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin.ml +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Formula.cmi +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Formula.cmt +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Formula.cmti +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Formula.cmx +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Ground.cmi +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Ground.cmt +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Ground.cmti +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Ground.cmx +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Instances.cmi +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Instances.cmt +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Instances.cmti +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Instances.cmx +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Rules.cmi +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Rules.cmt +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Rules.cmti +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Rules.cmx +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Sequent.cmi +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Sequent.cmt +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Sequent.cmti +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Sequent.cmx +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Unify.cmi +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Unify.cmt +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Unify.cmti +lib/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Unify.cmx +lib/rocq-runtime/plugins/firstorder_core/formula.ml +lib/rocq-runtime/plugins/firstorder_core/formula.mli +lib/rocq-runtime/plugins/firstorder_core/ground.ml +lib/rocq-runtime/plugins/firstorder_core/ground.mli +lib/rocq-runtime/plugins/firstorder_core/instances.ml +lib/rocq-runtime/plugins/firstorder_core/instances.mli +lib/rocq-runtime/plugins/firstorder_core/rules.ml +lib/rocq-runtime/plugins/firstorder_core/rules.mli +lib/rocq-runtime/plugins/firstorder_core/sequent.ml +lib/rocq-runtime/plugins/firstorder_core/sequent.mli +lib/rocq-runtime/plugins/firstorder_core/unify.ml +lib/rocq-runtime/plugins/firstorder_core/unify.mli +lib/rocq-runtime/plugins/funind/functional_principles_proofs.ml +lib/rocq-runtime/plugins/funind/functional_principles_proofs.mli +lib/rocq-runtime/plugins/funind/functional_principles_types.ml +lib/rocq-runtime/plugins/funind/functional_principles_types.mli +lib/rocq-runtime/plugins/funind/funind_plugin.a +lib/rocq-runtime/plugins/funind/funind_plugin.cma +lib/rocq-runtime/plugins/funind/funind_plugin.cmi +lib/rocq-runtime/plugins/funind/funind_plugin.cmt +lib/rocq-runtime/plugins/funind/funind_plugin.cmx +lib/rocq-runtime/plugins/funind/funind_plugin.cmxa +lib/rocq-runtime/plugins/funind/funind_plugin.cmxs +lib/rocq-runtime/plugins/funind/funind_plugin.ml +lib/rocq-runtime/plugins/funind/funind_plugin__Functional_principles_proofs.cmi +lib/rocq-runtime/plugins/funind/funind_plugin__Functional_principles_proofs.cmt +lib/rocq-runtime/plugins/funind/funind_plugin__Functional_principles_proofs.cmti +lib/rocq-runtime/plugins/funind/funind_plugin__Functional_principles_proofs.cmx +lib/rocq-runtime/plugins/funind/funind_plugin__Functional_principles_types.cmi +lib/rocq-runtime/plugins/funind/funind_plugin__Functional_principles_types.cmt +lib/rocq-runtime/plugins/funind/funind_plugin__Functional_principles_types.cmti +lib/rocq-runtime/plugins/funind/funind_plugin__Functional_principles_types.cmx +lib/rocq-runtime/plugins/funind/funind_plugin__G_indfun.cmi +lib/rocq-runtime/plugins/funind/funind_plugin__G_indfun.cmt +lib/rocq-runtime/plugins/funind/funind_plugin__G_indfun.cmti +lib/rocq-runtime/plugins/funind/funind_plugin__G_indfun.cmx +lib/rocq-runtime/plugins/funind/funind_plugin__Gen_principle.cmi +lib/rocq-runtime/plugins/funind/funind_plugin__Gen_principle.cmt +lib/rocq-runtime/plugins/funind/funind_plugin__Gen_principle.cmti +lib/rocq-runtime/plugins/funind/funind_plugin__Gen_principle.cmx +lib/rocq-runtime/plugins/funind/funind_plugin__Glob_term_to_relation.cmi +lib/rocq-runtime/plugins/funind/funind_plugin__Glob_term_to_relation.cmt +lib/rocq-runtime/plugins/funind/funind_plugin__Glob_term_to_relation.cmti +lib/rocq-runtime/plugins/funind/funind_plugin__Glob_term_to_relation.cmx +lib/rocq-runtime/plugins/funind/funind_plugin__Glob_termops.cmi +lib/rocq-runtime/plugins/funind/funind_plugin__Glob_termops.cmt +lib/rocq-runtime/plugins/funind/funind_plugin__Glob_termops.cmti +lib/rocq-runtime/plugins/funind/funind_plugin__Glob_termops.cmx +lib/rocq-runtime/plugins/funind/funind_plugin__Indfun.cmi +lib/rocq-runtime/plugins/funind/funind_plugin__Indfun.cmt +lib/rocq-runtime/plugins/funind/funind_plugin__Indfun.cmti +lib/rocq-runtime/plugins/funind/funind_plugin__Indfun.cmx +lib/rocq-runtime/plugins/funind/funind_plugin__Indfun_common.cmi +lib/rocq-runtime/plugins/funind/funind_plugin__Indfun_common.cmt +lib/rocq-runtime/plugins/funind/funind_plugin__Indfun_common.cmti +lib/rocq-runtime/plugins/funind/funind_plugin__Indfun_common.cmx +lib/rocq-runtime/plugins/funind/funind_plugin__Invfun.cmi +lib/rocq-runtime/plugins/funind/funind_plugin__Invfun.cmt +lib/rocq-runtime/plugins/funind/funind_plugin__Invfun.cmti +lib/rocq-runtime/plugins/funind/funind_plugin__Invfun.cmx +lib/rocq-runtime/plugins/funind/funind_plugin__Recdef.cmi +lib/rocq-runtime/plugins/funind/funind_plugin__Recdef.cmt +lib/rocq-runtime/plugins/funind/funind_plugin__Recdef.cmti +lib/rocq-runtime/plugins/funind/funind_plugin__Recdef.cmx +lib/rocq-runtime/plugins/funind/g_indfun.ml +lib/rocq-runtime/plugins/funind/g_indfun.mli +lib/rocq-runtime/plugins/funind/gen_principle.ml +lib/rocq-runtime/plugins/funind/gen_principle.mli +lib/rocq-runtime/plugins/funind/glob_term_to_relation.ml +lib/rocq-runtime/plugins/funind/glob_term_to_relation.mli +lib/rocq-runtime/plugins/funind/glob_termops.ml +lib/rocq-runtime/plugins/funind/glob_termops.mli +lib/rocq-runtime/plugins/funind/indfun.ml +lib/rocq-runtime/plugins/funind/indfun.mli +lib/rocq-runtime/plugins/funind/indfun_common.ml +lib/rocq-runtime/plugins/funind/indfun_common.mli +lib/rocq-runtime/plugins/funind/invfun.ml +lib/rocq-runtime/plugins/funind/invfun.mli +lib/rocq-runtime/plugins/funind/recdef.ml +lib/rocq-runtime/plugins/funind/recdef.mli +lib/rocq-runtime/plugins/ltac/comRewrite.ml +lib/rocq-runtime/plugins/ltac/comRewrite.mli +lib/rocq-runtime/plugins/ltac/coretactics.ml +lib/rocq-runtime/plugins/ltac/coretactics.mli +lib/rocq-runtime/plugins/ltac/extraargs.ml +lib/rocq-runtime/plugins/ltac/extraargs.mli +lib/rocq-runtime/plugins/ltac/extratactics.ml +lib/rocq-runtime/plugins/ltac/extratactics.mli +lib/rocq-runtime/plugins/ltac/g_auto.ml +lib/rocq-runtime/plugins/ltac/g_auto.mli +lib/rocq-runtime/plugins/ltac/g_class.ml +lib/rocq-runtime/plugins/ltac/g_class.mli +lib/rocq-runtime/plugins/ltac/g_eqdecide.ml +lib/rocq-runtime/plugins/ltac/g_eqdecide.mli +lib/rocq-runtime/plugins/ltac/g_ltac.ml +lib/rocq-runtime/plugins/ltac/g_ltac.mli +lib/rocq-runtime/plugins/ltac/g_rewrite.ml +lib/rocq-runtime/plugins/ltac/g_rewrite.mli +lib/rocq-runtime/plugins/ltac/g_tactic.ml +lib/rocq-runtime/plugins/ltac/g_tactic.mli +lib/rocq-runtime/plugins/ltac/internals.ml +lib/rocq-runtime/plugins/ltac/internals.mli +lib/rocq-runtime/plugins/ltac/leminv.ml +lib/rocq-runtime/plugins/ltac/leminv.mli +lib/rocq-runtime/plugins/ltac/ltac_plugin.a +lib/rocq-runtime/plugins/ltac/ltac_plugin.cma +lib/rocq-runtime/plugins/ltac/ltac_plugin.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin.cmxa +lib/rocq-runtime/plugins/ltac/ltac_plugin.cmxs +lib/rocq-runtime/plugins/ltac/ltac_plugin.ml +lib/rocq-runtime/plugins/ltac/ltac_plugin__ComRewrite.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__ComRewrite.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__ComRewrite.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__ComRewrite.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Coretactics.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Coretactics.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Coretactics.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Coretactics.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Extraargs.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Extraargs.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Extraargs.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Extraargs.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Extratactics.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Extratactics.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Extratactics.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Extratactics.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_auto.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_auto.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_auto.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_auto.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_class.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_class.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_class.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_class.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_eqdecide.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_eqdecide.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_eqdecide.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_eqdecide.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_ltac.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_ltac.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_ltac.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_ltac.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_rewrite.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_rewrite.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_rewrite.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_rewrite.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_tactic.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_tactic.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_tactic.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__G_tactic.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Internals.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Internals.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Internals.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Internals.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Leminv.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Leminv.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Leminv.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Leminv.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Pltac.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Pltac.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Pltac.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Pltac.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Pptactic.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Pptactic.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Pptactic.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Pptactic.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Profile_ltac_tactics.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Profile_ltac_tactics.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Profile_ltac_tactics.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Profile_ltac_tactics.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacarg.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacarg.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacarg.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacarg.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Taccoerce.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Taccoerce.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Taccoerce.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Taccoerce.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacentries.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacentries.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacentries.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacentries.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacenv.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacenv.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacenv.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacenv.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacexpr.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacexpr.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacintern.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacintern.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacintern.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacintern.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacinterp.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacinterp.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacinterp.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacinterp.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacsubst.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacsubst.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacsubst.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tacsubst.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tactic_debug.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tactic_debug.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tactic_debug.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tactic_debug.cmx +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tactic_matching.cmi +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tactic_matching.cmt +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tactic_matching.cmti +lib/rocq-runtime/plugins/ltac/ltac_plugin__Tactic_matching.cmx +lib/rocq-runtime/plugins/ltac/pltac.ml +lib/rocq-runtime/plugins/ltac/pltac.mli +lib/rocq-runtime/plugins/ltac/pptactic.ml +lib/rocq-runtime/plugins/ltac/pptactic.mli +lib/rocq-runtime/plugins/ltac/profile_ltac_tactics.ml +lib/rocq-runtime/plugins/ltac/profile_ltac_tactics.mli +lib/rocq-runtime/plugins/ltac/tacarg.ml +lib/rocq-runtime/plugins/ltac/tacarg.mli +lib/rocq-runtime/plugins/ltac/taccoerce.ml +lib/rocq-runtime/plugins/ltac/taccoerce.mli +lib/rocq-runtime/plugins/ltac/tacentries.ml +lib/rocq-runtime/plugins/ltac/tacentries.mli +lib/rocq-runtime/plugins/ltac/tacenv.ml +lib/rocq-runtime/plugins/ltac/tacenv.mli +lib/rocq-runtime/plugins/ltac/tacexpr.mli +lib/rocq-runtime/plugins/ltac/tacintern.ml +lib/rocq-runtime/plugins/ltac/tacintern.mli +lib/rocq-runtime/plugins/ltac/tacinterp.ml +lib/rocq-runtime/plugins/ltac/tacinterp.mli +lib/rocq-runtime/plugins/ltac/tacsubst.ml +lib/rocq-runtime/plugins/ltac/tacsubst.mli +lib/rocq-runtime/plugins/ltac/tactic_debug.ml +lib/rocq-runtime/plugins/ltac/tactic_debug.mli +lib/rocq-runtime/plugins/ltac/tactic_matching.ml +lib/rocq-runtime/plugins/ltac/tactic_matching.mli +lib/rocq-runtime/plugins/ltac2/g_ltac2.ml +lib/rocq-runtime/plugins/ltac2/g_ltac2.mli +lib/rocq-runtime/plugins/ltac2/ltac2_plugin.a +lib/rocq-runtime/plugins/ltac2/ltac2_plugin.cma +lib/rocq-runtime/plugins/ltac2/ltac2_plugin.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin.cmxa +lib/rocq-runtime/plugins/ltac2/ltac2_plugin.cmxs +lib/rocq-runtime/plugins/ltac2/ltac2_plugin.ml +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__G_ltac2.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__G_ltac2.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__G_ltac2.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__G_ltac2.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2bt.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2bt.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2bt.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2bt.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2core.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2core.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2core.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2core.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2dyn.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2dyn.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2dyn.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2dyn.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2entries.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2entries.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2entries.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2entries.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2env.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2env.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2env.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2env.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2expr.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2expr.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2externals.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2externals.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2externals.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2externals.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2extffi.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2extffi.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2extffi.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2extffi.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2ffi.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2ffi.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2ffi.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2ffi.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2intern.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2intern.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2intern.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2intern.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2interp.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2interp.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2interp.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2interp.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2match.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2match.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2match.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2match.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2print.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2print.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2print.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2print.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2qexpr.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2qexpr.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2quote.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2quote.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2quote.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2quote.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2stdlib.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2stdlib.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2stdlib.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2stdlib.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2tactics.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2tactics.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2tactics.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2tactics.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2types.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2types.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2typing_env.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2typing_env.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2typing_env.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2typing_env.cmx +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2val.cmi +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2val.cmt +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2val.cmti +lib/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2val.cmx +lib/rocq-runtime/plugins/ltac2/tac2bt.ml +lib/rocq-runtime/plugins/ltac2/tac2bt.mli +lib/rocq-runtime/plugins/ltac2/tac2core.ml +lib/rocq-runtime/plugins/ltac2/tac2core.mli +lib/rocq-runtime/plugins/ltac2/tac2dyn.ml +lib/rocq-runtime/plugins/ltac2/tac2dyn.mli +lib/rocq-runtime/plugins/ltac2/tac2entries.ml +lib/rocq-runtime/plugins/ltac2/tac2entries.mli +lib/rocq-runtime/plugins/ltac2/tac2env.ml +lib/rocq-runtime/plugins/ltac2/tac2env.mli +lib/rocq-runtime/plugins/ltac2/tac2expr.mli +lib/rocq-runtime/plugins/ltac2/tac2externals.ml +lib/rocq-runtime/plugins/ltac2/tac2externals.mli +lib/rocq-runtime/plugins/ltac2/tac2extffi.ml +lib/rocq-runtime/plugins/ltac2/tac2extffi.mli +lib/rocq-runtime/plugins/ltac2/tac2ffi.ml +lib/rocq-runtime/plugins/ltac2/tac2ffi.mli +lib/rocq-runtime/plugins/ltac2/tac2intern.ml +lib/rocq-runtime/plugins/ltac2/tac2intern.mli +lib/rocq-runtime/plugins/ltac2/tac2interp.ml +lib/rocq-runtime/plugins/ltac2/tac2interp.mli +lib/rocq-runtime/plugins/ltac2/tac2match.ml +lib/rocq-runtime/plugins/ltac2/tac2match.mli +lib/rocq-runtime/plugins/ltac2/tac2print.ml +lib/rocq-runtime/plugins/ltac2/tac2print.mli +lib/rocq-runtime/plugins/ltac2/tac2qexpr.mli +lib/rocq-runtime/plugins/ltac2/tac2quote.ml +lib/rocq-runtime/plugins/ltac2/tac2quote.mli +lib/rocq-runtime/plugins/ltac2/tac2stdlib.ml +lib/rocq-runtime/plugins/ltac2/tac2stdlib.mli +lib/rocq-runtime/plugins/ltac2/tac2tactics.ml +lib/rocq-runtime/plugins/ltac2/tac2tactics.mli +lib/rocq-runtime/plugins/ltac2/tac2types.mli +lib/rocq-runtime/plugins/ltac2/tac2typing_env.ml +lib/rocq-runtime/plugins/ltac2/tac2typing_env.mli +lib/rocq-runtime/plugins/ltac2/tac2val.ml +lib/rocq-runtime/plugins/ltac2/tac2val.mli +lib/rocq-runtime/plugins/ltac2_ltac1/g_ltac2_ltac1.ml +lib/rocq-runtime/plugins/ltac2_ltac1/g_ltac2_ltac1.mli +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin.a +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cma +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmi +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmt +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmx +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmxa +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmxs +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin.ml +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__G_ltac2_ltac1.cmi +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__G_ltac2_ltac1.cmt +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__G_ltac2_ltac1.cmti +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__G_ltac2_ltac1.cmx +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2core_ltac1.cmi +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2core_ltac1.cmt +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2core_ltac1.cmti +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2core_ltac1.cmx +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2quote_ltac1.cmi +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2quote_ltac1.cmt +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2quote_ltac1.cmti +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2quote_ltac1.cmx +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2stdlib_ltac1.cmi +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2stdlib_ltac1.cmt +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2stdlib_ltac1.cmti +lib/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2stdlib_ltac1.cmx +lib/rocq-runtime/plugins/ltac2_ltac1/tac2core_ltac1.ml +lib/rocq-runtime/plugins/ltac2_ltac1/tac2core_ltac1.mli +lib/rocq-runtime/plugins/ltac2_ltac1/tac2quote_ltac1.ml +lib/rocq-runtime/plugins/ltac2_ltac1/tac2quote_ltac1.mli +lib/rocq-runtime/plugins/ltac2_ltac1/tac2stdlib_ltac1.ml +lib/rocq-runtime/plugins/ltac2_ltac1/tac2stdlib_ltac1.mli +lib/rocq-runtime/plugins/micromega/certificate.ml +lib/rocq-runtime/plugins/micromega/certificate.mli +lib/rocq-runtime/plugins/micromega/coq_micromega.ml +lib/rocq-runtime/plugins/micromega/coq_micromega.mli +lib/rocq-runtime/plugins/micromega/g_micromega.ml +lib/rocq-runtime/plugins/micromega/g_micromega.mli +lib/rocq-runtime/plugins/micromega/itv.ml +lib/rocq-runtime/plugins/micromega/itv.mli +lib/rocq-runtime/plugins/micromega/linsolve.ml +lib/rocq-runtime/plugins/micromega/linsolve.mli +lib/rocq-runtime/plugins/micromega/micromega_plugin.a +lib/rocq-runtime/plugins/micromega/micromega_plugin.cma +lib/rocq-runtime/plugins/micromega/micromega_plugin.cmi +lib/rocq-runtime/plugins/micromega/micromega_plugin.cmt +lib/rocq-runtime/plugins/micromega/micromega_plugin.cmx +lib/rocq-runtime/plugins/micromega/micromega_plugin.cmxa +lib/rocq-runtime/plugins/micromega/micromega_plugin.cmxs +lib/rocq-runtime/plugins/micromega/micromega_plugin.ml +lib/rocq-runtime/plugins/micromega/micromega_plugin__Certificate.cmi +lib/rocq-runtime/plugins/micromega/micromega_plugin__Certificate.cmt +lib/rocq-runtime/plugins/micromega/micromega_plugin__Certificate.cmti +lib/rocq-runtime/plugins/micromega/micromega_plugin__Certificate.cmx +lib/rocq-runtime/plugins/micromega/micromega_plugin__Coq_micromega.cmi +lib/rocq-runtime/plugins/micromega/micromega_plugin__Coq_micromega.cmt +lib/rocq-runtime/plugins/micromega/micromega_plugin__Coq_micromega.cmti +lib/rocq-runtime/plugins/micromega/micromega_plugin__Coq_micromega.cmx +lib/rocq-runtime/plugins/micromega/micromega_plugin__G_micromega.cmi +lib/rocq-runtime/plugins/micromega/micromega_plugin__G_micromega.cmt +lib/rocq-runtime/plugins/micromega/micromega_plugin__G_micromega.cmti +lib/rocq-runtime/plugins/micromega/micromega_plugin__G_micromega.cmx +lib/rocq-runtime/plugins/micromega/micromega_plugin__Itv.cmi +lib/rocq-runtime/plugins/micromega/micromega_plugin__Itv.cmt +lib/rocq-runtime/plugins/micromega/micromega_plugin__Itv.cmti +lib/rocq-runtime/plugins/micromega/micromega_plugin__Itv.cmx +lib/rocq-runtime/plugins/micromega/micromega_plugin__Linsolve.cmi +lib/rocq-runtime/plugins/micromega/micromega_plugin__Linsolve.cmt +lib/rocq-runtime/plugins/micromega/micromega_plugin__Linsolve.cmti +lib/rocq-runtime/plugins/micromega/micromega_plugin__Linsolve.cmx +lib/rocq-runtime/plugins/micromega/micromega_plugin__Persistent_cache.cmi +lib/rocq-runtime/plugins/micromega/micromega_plugin__Persistent_cache.cmt +lib/rocq-runtime/plugins/micromega/micromega_plugin__Persistent_cache.cmti +lib/rocq-runtime/plugins/micromega/micromega_plugin__Persistent_cache.cmx +lib/rocq-runtime/plugins/micromega/micromega_plugin__Polynomial.cmi +lib/rocq-runtime/plugins/micromega/micromega_plugin__Polynomial.cmt +lib/rocq-runtime/plugins/micromega/micromega_plugin__Polynomial.cmti +lib/rocq-runtime/plugins/micromega/micromega_plugin__Polynomial.cmx +lib/rocq-runtime/plugins/micromega/micromega_plugin__Simplex.cmi +lib/rocq-runtime/plugins/micromega/micromega_plugin__Simplex.cmt +lib/rocq-runtime/plugins/micromega/micromega_plugin__Simplex.cmti +lib/rocq-runtime/plugins/micromega/micromega_plugin__Simplex.cmx +lib/rocq-runtime/plugins/micromega/micromega_plugin__Vect.cmi +lib/rocq-runtime/plugins/micromega/micromega_plugin__Vect.cmt +lib/rocq-runtime/plugins/micromega/micromega_plugin__Vect.cmti +lib/rocq-runtime/plugins/micromega/micromega_plugin__Vect.cmx +lib/rocq-runtime/plugins/micromega/persistent_cache.ml +lib/rocq-runtime/plugins/micromega/persistent_cache.mli +lib/rocq-runtime/plugins/micromega/polynomial.ml +lib/rocq-runtime/plugins/micromega/polynomial.mli +lib/rocq-runtime/plugins/micromega/simplex.ml +lib/rocq-runtime/plugins/micromega/simplex.mli +lib/rocq-runtime/plugins/micromega/vect.ml +lib/rocq-runtime/plugins/micromega/vect.mli +lib/rocq-runtime/plugins/micromega_core/micromega.ml +lib/rocq-runtime/plugins/micromega_core/micromega.mli +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin.a +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin.cma +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin.cmi +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin.cmt +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin.cmx +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin.cmxa +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin.cmxs +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin.ml +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Micromega.cmi +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Micromega.cmt +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Micromega.cmti +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Micromega.cmx +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Mutils.cmi +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Mutils.cmt +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Mutils.cmti +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Mutils.cmx +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__NumCompat.cmi +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__NumCompat.cmt +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__NumCompat.cmti +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__NumCompat.cmx +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos.cmi +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos.cmt +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos.cmti +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos.cmx +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos_lib.cmi +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos_lib.cmt +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos_lib.cmti +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos_lib.cmx +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos_types.cmi +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos_types.cmt +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos_types.cmti +lib/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos_types.cmx +lib/rocq-runtime/plugins/micromega_core/mutils.ml +lib/rocq-runtime/plugins/micromega_core/mutils.mli +lib/rocq-runtime/plugins/micromega_core/numCompat.ml +lib/rocq-runtime/plugins/micromega_core/numCompat.mli +lib/rocq-runtime/plugins/micromega_core/sos.ml +lib/rocq-runtime/plugins/micromega_core/sos.mli +lib/rocq-runtime/plugins/micromega_core/sos_lib.ml +lib/rocq-runtime/plugins/micromega_core/sos_lib.mli +lib/rocq-runtime/plugins/micromega_core/sos_types.ml +lib/rocq-runtime/plugins/micromega_core/sos_types.mli +lib/rocq-runtime/plugins/nsatz/g_nsatz.ml +lib/rocq-runtime/plugins/nsatz/g_nsatz.mli +lib/rocq-runtime/plugins/nsatz/nsatz_plugin.a +lib/rocq-runtime/plugins/nsatz/nsatz_plugin.cma +lib/rocq-runtime/plugins/nsatz/nsatz_plugin.cmi +lib/rocq-runtime/plugins/nsatz/nsatz_plugin.cmt +lib/rocq-runtime/plugins/nsatz/nsatz_plugin.cmx +lib/rocq-runtime/plugins/nsatz/nsatz_plugin.cmxa +lib/rocq-runtime/plugins/nsatz/nsatz_plugin.cmxs +lib/rocq-runtime/plugins/nsatz/nsatz_plugin.ml +lib/rocq-runtime/plugins/nsatz/nsatz_plugin__G_nsatz.cmi +lib/rocq-runtime/plugins/nsatz/nsatz_plugin__G_nsatz.cmt +lib/rocq-runtime/plugins/nsatz/nsatz_plugin__G_nsatz.cmti +lib/rocq-runtime/plugins/nsatz/nsatz_plugin__G_nsatz.cmx +lib/rocq-runtime/plugins/nsatz_core/ideal.ml +lib/rocq-runtime/plugins/nsatz_core/ideal.mli +lib/rocq-runtime/plugins/nsatz_core/nsatz.ml +lib/rocq-runtime/plugins/nsatz_core/nsatz.mli +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin.a +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin.cma +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin.cmi +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin.cmt +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin.cmx +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin.cmxa +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin.cmxs +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin.ml +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Ideal.cmi +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Ideal.cmt +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Ideal.cmti +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Ideal.cmx +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Nsatz.cmi +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Nsatz.cmt +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Nsatz.cmti +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Nsatz.cmx +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Polynom.cmi +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Polynom.cmt +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Polynom.cmti +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Polynom.cmx +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Utile.cmi +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Utile.cmt +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Utile.cmti +lib/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Utile.cmx +lib/rocq-runtime/plugins/nsatz_core/polynom.ml +lib/rocq-runtime/plugins/nsatz_core/polynom.mli +lib/rocq-runtime/plugins/nsatz_core/utile.ml +lib/rocq-runtime/plugins/nsatz_core/utile.mli +lib/rocq-runtime/plugins/number_string_notation/g_number_string.ml +lib/rocq-runtime/plugins/number_string_notation/g_number_string.mli +lib/rocq-runtime/plugins/number_string_notation/number_string.ml +lib/rocq-runtime/plugins/number_string_notation/number_string.mli +lib/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin.a +lib/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin.cma +lib/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin.cmi +lib/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin.cmt +lib/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin.cmx +lib/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin.cmxa +lib/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin.cmxs +lib/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin.ml +lib/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin__G_number_string.cmi +lib/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin__G_number_string.cmt +lib/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin__G_number_string.cmti +lib/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin__G_number_string.cmx +lib/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin__Number_string.cmi +lib/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin__Number_string.cmt +lib/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin__Number_string.cmti +lib/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin__Number_string.cmx +lib/rocq-runtime/plugins/ring/g_ring.ml +lib/rocq-runtime/plugins/ring/g_ring.mli +lib/rocq-runtime/plugins/ring/ring.ml +lib/rocq-runtime/plugins/ring/ring.mli +lib/rocq-runtime/plugins/ring/ring_ast.ml +lib/rocq-runtime/plugins/ring/ring_ast.mli +lib/rocq-runtime/plugins/ring/ring_plugin.a +lib/rocq-runtime/plugins/ring/ring_plugin.cma +lib/rocq-runtime/plugins/ring/ring_plugin.cmi +lib/rocq-runtime/plugins/ring/ring_plugin.cmt +lib/rocq-runtime/plugins/ring/ring_plugin.cmx +lib/rocq-runtime/plugins/ring/ring_plugin.cmxa +lib/rocq-runtime/plugins/ring/ring_plugin.cmxs +lib/rocq-runtime/plugins/ring/ring_plugin.ml +lib/rocq-runtime/plugins/ring/ring_plugin__G_ring.cmi +lib/rocq-runtime/plugins/ring/ring_plugin__G_ring.cmt +lib/rocq-runtime/plugins/ring/ring_plugin__G_ring.cmti +lib/rocq-runtime/plugins/ring/ring_plugin__G_ring.cmx +lib/rocq-runtime/plugins/ring/ring_plugin__Ring.cmi +lib/rocq-runtime/plugins/ring/ring_plugin__Ring.cmt +lib/rocq-runtime/plugins/ring/ring_plugin__Ring.cmti +lib/rocq-runtime/plugins/ring/ring_plugin__Ring.cmx +lib/rocq-runtime/plugins/ring/ring_plugin__Ring_ast.cmi +lib/rocq-runtime/plugins/ring/ring_plugin__Ring_ast.cmt +lib/rocq-runtime/plugins/ring/ring_plugin__Ring_ast.cmti +lib/rocq-runtime/plugins/ring/ring_plugin__Ring_ast.cmx +lib/rocq-runtime/plugins/rtauto/g_rtauto.ml +lib/rocq-runtime/plugins/rtauto/g_rtauto.mli +lib/rocq-runtime/plugins/rtauto/proof_search.ml +lib/rocq-runtime/plugins/rtauto/proof_search.mli +lib/rocq-runtime/plugins/rtauto/refl_tauto.ml +lib/rocq-runtime/plugins/rtauto/refl_tauto.mli +lib/rocq-runtime/plugins/rtauto/rtauto_plugin.a +lib/rocq-runtime/plugins/rtauto/rtauto_plugin.cma +lib/rocq-runtime/plugins/rtauto/rtauto_plugin.cmi +lib/rocq-runtime/plugins/rtauto/rtauto_plugin.cmt +lib/rocq-runtime/plugins/rtauto/rtauto_plugin.cmx +lib/rocq-runtime/plugins/rtauto/rtauto_plugin.cmxa +lib/rocq-runtime/plugins/rtauto/rtauto_plugin.cmxs +lib/rocq-runtime/plugins/rtauto/rtauto_plugin.ml +lib/rocq-runtime/plugins/rtauto/rtauto_plugin__G_rtauto.cmi +lib/rocq-runtime/plugins/rtauto/rtauto_plugin__G_rtauto.cmt +lib/rocq-runtime/plugins/rtauto/rtauto_plugin__G_rtauto.cmti +lib/rocq-runtime/plugins/rtauto/rtauto_plugin__G_rtauto.cmx +lib/rocq-runtime/plugins/rtauto/rtauto_plugin__Proof_search.cmi +lib/rocq-runtime/plugins/rtauto/rtauto_plugin__Proof_search.cmt +lib/rocq-runtime/plugins/rtauto/rtauto_plugin__Proof_search.cmti +lib/rocq-runtime/plugins/rtauto/rtauto_plugin__Proof_search.cmx +lib/rocq-runtime/plugins/rtauto/rtauto_plugin__Refl_tauto.cmi +lib/rocq-runtime/plugins/rtauto/rtauto_plugin__Refl_tauto.cmt +lib/rocq-runtime/plugins/rtauto/rtauto_plugin__Refl_tauto.cmti +lib/rocq-runtime/plugins/rtauto/rtauto_plugin__Refl_tauto.cmx +lib/rocq-runtime/plugins/ssreflect/ssrast.mli +lib/rocq-runtime/plugins/ssreflect/ssrbwd.ml +lib/rocq-runtime/plugins/ssreflect/ssrbwd.mli +lib/rocq-runtime/plugins/ssreflect/ssrcommon.ml +lib/rocq-runtime/plugins/ssreflect/ssrcommon.mli +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin.a +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin.cma +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin.cmi +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin.cmt +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin.cmx +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin.cmxa +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin.cmxs +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin.ml +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrast.cmi +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrast.cmti +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrbwd.cmi +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrbwd.cmt +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrbwd.cmti +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrbwd.cmx +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrcommon.cmi +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrcommon.cmt +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrcommon.cmti +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrcommon.cmx +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrelim.cmi +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrelim.cmt +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrelim.cmti +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrelim.cmx +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrequality.cmi +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrequality.cmt +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrequality.cmti +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrequality.cmx +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrfwd.cmi +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrfwd.cmt +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrfwd.cmti +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrfwd.cmx +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssripats.cmi +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssripats.cmt +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssripats.cmti +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssripats.cmx +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrparser.cmi +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrparser.cmt +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrparser.cmti +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrparser.cmx +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrprinters.cmi +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrprinters.cmt +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrprinters.cmti +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrprinters.cmx +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrtacs.cmi +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrtacs.cmt +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrtacs.cmti +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrtacs.cmx +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrtacticals.cmi +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrtacticals.cmt +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrtacticals.cmti +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrtacticals.cmx +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrvernac.cmi +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrvernac.cmt +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrvernac.cmti +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrvernac.cmx +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrview.cmi +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrview.cmt +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrview.cmti +lib/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrview.cmx +lib/rocq-runtime/plugins/ssreflect/ssrelim.ml +lib/rocq-runtime/plugins/ssreflect/ssrelim.mli +lib/rocq-runtime/plugins/ssreflect/ssrequality.ml +lib/rocq-runtime/plugins/ssreflect/ssrequality.mli +lib/rocq-runtime/plugins/ssreflect/ssrfwd.ml +lib/rocq-runtime/plugins/ssreflect/ssrfwd.mli +lib/rocq-runtime/plugins/ssreflect/ssripats.ml +lib/rocq-runtime/plugins/ssreflect/ssripats.mli +lib/rocq-runtime/plugins/ssreflect/ssrparser.ml +lib/rocq-runtime/plugins/ssreflect/ssrparser.mli +lib/rocq-runtime/plugins/ssreflect/ssrprinters.ml +lib/rocq-runtime/plugins/ssreflect/ssrprinters.mli +lib/rocq-runtime/plugins/ssreflect/ssrtacs.ml +lib/rocq-runtime/plugins/ssreflect/ssrtacs.mli +lib/rocq-runtime/plugins/ssreflect/ssrtacticals.ml +lib/rocq-runtime/plugins/ssreflect/ssrtacticals.mli +lib/rocq-runtime/plugins/ssreflect/ssrvernac.ml +lib/rocq-runtime/plugins/ssreflect/ssrvernac.mli +lib/rocq-runtime/plugins/ssreflect/ssrview.ml +lib/rocq-runtime/plugins/ssreflect/ssrview.mli +lib/rocq-runtime/plugins/ssrmatching/g_ssrmatching.ml +lib/rocq-runtime/plugins/ssrmatching/g_ssrmatching.mli +lib/rocq-runtime/plugins/ssrmatching/ssrmatching.ml +lib/rocq-runtime/plugins/ssrmatching/ssrmatching.mli +lib/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin.a +lib/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin.cma +lib/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin.cmi +lib/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin.cmt +lib/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin.cmx +lib/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin.cmxa +lib/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin.cmxs +lib/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin.ml +lib/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin__G_ssrmatching.cmi +lib/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin__G_ssrmatching.cmt +lib/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin__G_ssrmatching.cmti +lib/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin__G_ssrmatching.cmx +lib/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin__Ssrmatching.cmi +lib/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin__Ssrmatching.cmt +lib/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin__Ssrmatching.cmti +lib/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin__Ssrmatching.cmx +lib/rocq-runtime/plugins/tauto/tauto.ml +lib/rocq-runtime/plugins/tauto/tauto.mli +lib/rocq-runtime/plugins/tauto/tauto_plugin.a +lib/rocq-runtime/plugins/tauto/tauto_plugin.cma +lib/rocq-runtime/plugins/tauto/tauto_plugin.cmi +lib/rocq-runtime/plugins/tauto/tauto_plugin.cmt +lib/rocq-runtime/plugins/tauto/tauto_plugin.cmx +lib/rocq-runtime/plugins/tauto/tauto_plugin.cmxa +lib/rocq-runtime/plugins/tauto/tauto_plugin.cmxs +lib/rocq-runtime/plugins/tauto/tauto_plugin.ml +lib/rocq-runtime/plugins/tauto/tauto_plugin__Tauto.cmi +lib/rocq-runtime/plugins/tauto/tauto_plugin__Tauto.cmt +lib/rocq-runtime/plugins/tauto/tauto_plugin__Tauto.cmti +lib/rocq-runtime/plugins/tauto/tauto_plugin__Tauto.cmx +lib/rocq-runtime/plugins/tutorial/p0/g_tuto0.ml +lib/rocq-runtime/plugins/tutorial/p0/tuto0_main.ml +lib/rocq-runtime/plugins/tutorial/p0/tuto0_main.mli +lib/rocq-runtime/plugins/tutorial/p0/tuto0_plugin.a +lib/rocq-runtime/plugins/tutorial/p0/tuto0_plugin.cma +lib/rocq-runtime/plugins/tutorial/p0/tuto0_plugin.cmi +lib/rocq-runtime/plugins/tutorial/p0/tuto0_plugin.cmt +lib/rocq-runtime/plugins/tutorial/p0/tuto0_plugin.cmx +lib/rocq-runtime/plugins/tutorial/p0/tuto0_plugin.cmxa +lib/rocq-runtime/plugins/tutorial/p0/tuto0_plugin.cmxs +lib/rocq-runtime/plugins/tutorial/p0/tuto0_plugin.ml +lib/rocq-runtime/plugins/tutorial/p0/tuto0_plugin__G_tuto0.cmi +lib/rocq-runtime/plugins/tutorial/p0/tuto0_plugin__G_tuto0.cmt +lib/rocq-runtime/plugins/tutorial/p0/tuto0_plugin__G_tuto0.cmx +lib/rocq-runtime/plugins/tutorial/p0/tuto0_plugin__Tuto0_main.cmi +lib/rocq-runtime/plugins/tutorial/p0/tuto0_plugin__Tuto0_main.cmt +lib/rocq-runtime/plugins/tutorial/p0/tuto0_plugin__Tuto0_main.cmti +lib/rocq-runtime/plugins/tutorial/p0/tuto0_plugin__Tuto0_main.cmx +lib/rocq-runtime/plugins/tutorial/p1/g_tuto1.ml +lib/rocq-runtime/plugins/tutorial/p1/inspector.ml +lib/rocq-runtime/plugins/tutorial/p1/inspector.mli +lib/rocq-runtime/plugins/tutorial/p1/simple_check.ml +lib/rocq-runtime/plugins/tutorial/p1/simple_check.mli +lib/rocq-runtime/plugins/tutorial/p1/simple_declare.ml +lib/rocq-runtime/plugins/tutorial/p1/simple_declare.mli +lib/rocq-runtime/plugins/tutorial/p1/simple_print.ml +lib/rocq-runtime/plugins/tutorial/p1/simple_print.mli +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin.a +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin.cma +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin.cmi +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin.cmt +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin.cmx +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin.cmxa +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin.cmxs +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin.ml +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__G_tuto1.cmi +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__G_tuto1.cmt +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__G_tuto1.cmx +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Inspector.cmi +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Inspector.cmt +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Inspector.cmti +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Inspector.cmx +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_check.cmi +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_check.cmt +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_check.cmti +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_check.cmx +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_declare.cmi +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_declare.cmt +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_declare.cmti +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_declare.cmx +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_print.cmi +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_print.cmt +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_print.cmti +lib/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_print.cmx +lib/rocq-runtime/plugins/tutorial/p2/counter.ml +lib/rocq-runtime/plugins/tutorial/p2/counter.mli +lib/rocq-runtime/plugins/tutorial/p2/custom.ml +lib/rocq-runtime/plugins/tutorial/p2/custom.mli +lib/rocq-runtime/plugins/tutorial/p2/g_tuto2.ml +lib/rocq-runtime/plugins/tutorial/p2/persistent_counter.ml +lib/rocq-runtime/plugins/tutorial/p2/persistent_counter.mli +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin.a +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin.cma +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin.cmi +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin.cmt +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin.cmx +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin.cmxa +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin.cmxs +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin.ml +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Counter.cmi +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Counter.cmt +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Counter.cmti +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Counter.cmx +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Custom.cmi +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Custom.cmt +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Custom.cmti +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Custom.cmx +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__G_tuto2.cmi +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__G_tuto2.cmt +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__G_tuto2.cmx +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Persistent_counter.cmi +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Persistent_counter.cmt +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Persistent_counter.cmti +lib/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Persistent_counter.cmx +lib/rocq-runtime/plugins/tutorial/p3/construction_game.ml +lib/rocq-runtime/plugins/tutorial/p3/construction_game.mli +lib/rocq-runtime/plugins/tutorial/p3/g_tuto3.ml +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin.a +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin.cma +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin.cmi +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin.cmt +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin.cmx +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin.cmxa +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin.cmxs +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin.ml +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__Construction_game.cmi +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__Construction_game.cmt +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__Construction_game.cmti +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__Construction_game.cmx +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__G_tuto3.cmi +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__G_tuto3.cmt +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__G_tuto3.cmx +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__Tuto_tactic.cmi +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__Tuto_tactic.cmt +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__Tuto_tactic.cmti +lib/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__Tuto_tactic.cmx +lib/rocq-runtime/plugins/tutorial/p3/tuto_tactic.ml +lib/rocq-runtime/plugins/tutorial/p3/tuto_tactic.mli +lib/rocq-runtime/plugins/tutorial/p4/myexternals.ml +lib/rocq-runtime/plugins/tutorial/p4/myexternals.mli +lib/rocq-runtime/plugins/tutorial/p4/tuto4_plugin.a +lib/rocq-runtime/plugins/tutorial/p4/tuto4_plugin.cma +lib/rocq-runtime/plugins/tutorial/p4/tuto4_plugin.cmi +lib/rocq-runtime/plugins/tutorial/p4/tuto4_plugin.cmt +lib/rocq-runtime/plugins/tutorial/p4/tuto4_plugin.cmx +lib/rocq-runtime/plugins/tutorial/p4/tuto4_plugin.cmxa +lib/rocq-runtime/plugins/tutorial/p4/tuto4_plugin.cmxs +lib/rocq-runtime/plugins/tutorial/p4/tuto4_plugin.ml +lib/rocq-runtime/plugins/tutorial/p4/tuto4_plugin__Myexternals.cmi +lib/rocq-runtime/plugins/tutorial/p4/tuto4_plugin__Myexternals.cmt +lib/rocq-runtime/plugins/tutorial/p4/tuto4_plugin__Myexternals.cmti +lib/rocq-runtime/plugins/tutorial/p4/tuto4_plugin__Myexternals.cmx +lib/rocq-runtime/plugins/zify/g_zify.ml +lib/rocq-runtime/plugins/zify/g_zify.mli +lib/rocq-runtime/plugins/zify/zify.ml +lib/rocq-runtime/plugins/zify/zify.mli +lib/rocq-runtime/plugins/zify/zify_plugin.a +lib/rocq-runtime/plugins/zify/zify_plugin.cma +lib/rocq-runtime/plugins/zify/zify_plugin.cmi +lib/rocq-runtime/plugins/zify/zify_plugin.cmt +lib/rocq-runtime/plugins/zify/zify_plugin.cmx +lib/rocq-runtime/plugins/zify/zify_plugin.cmxa +lib/rocq-runtime/plugins/zify/zify_plugin.cmxs +lib/rocq-runtime/plugins/zify/zify_plugin.ml +lib/rocq-runtime/plugins/zify/zify_plugin__G_zify.cmi +lib/rocq-runtime/plugins/zify/zify_plugin__G_zify.cmt +lib/rocq-runtime/plugins/zify/zify_plugin__G_zify.cmti +lib/rocq-runtime/plugins/zify/zify_plugin__G_zify.cmx +lib/rocq-runtime/plugins/zify/zify_plugin__Zify.cmi +lib/rocq-runtime/plugins/zify/zify_plugin__Zify.cmt +lib/rocq-runtime/plugins/zify/zify_plugin__Zify.cmti +lib/rocq-runtime/plugins/zify/zify_plugin__Zify.cmx +lib/rocq-runtime/pretyping/arguments_renaming.cmi +lib/rocq-runtime/pretyping/arguments_renaming.cmt +lib/rocq-runtime/pretyping/arguments_renaming.cmti +lib/rocq-runtime/pretyping/arguments_renaming.cmx +lib/rocq-runtime/pretyping/arguments_renaming.ml +lib/rocq-runtime/pretyping/arguments_renaming.mli +lib/rocq-runtime/pretyping/cases.cmi +lib/rocq-runtime/pretyping/cases.cmt +lib/rocq-runtime/pretyping/cases.cmti +lib/rocq-runtime/pretyping/cases.cmx +lib/rocq-runtime/pretyping/cases.ml +lib/rocq-runtime/pretyping/cases.mli +lib/rocq-runtime/pretyping/cbv.cmi +lib/rocq-runtime/pretyping/cbv.cmt +lib/rocq-runtime/pretyping/cbv.cmti +lib/rocq-runtime/pretyping/cbv.cmx +lib/rocq-runtime/pretyping/cbv.ml +lib/rocq-runtime/pretyping/cbv.mli +lib/rocq-runtime/pretyping/coercion.cmi +lib/rocq-runtime/pretyping/coercion.cmt +lib/rocq-runtime/pretyping/coercion.cmti +lib/rocq-runtime/pretyping/coercion.cmx +lib/rocq-runtime/pretyping/coercion.ml +lib/rocq-runtime/pretyping/coercion.mli +lib/rocq-runtime/pretyping/coercionops.cmi +lib/rocq-runtime/pretyping/coercionops.cmt +lib/rocq-runtime/pretyping/coercionops.cmti +lib/rocq-runtime/pretyping/coercionops.cmx +lib/rocq-runtime/pretyping/coercionops.ml +lib/rocq-runtime/pretyping/coercionops.mli +lib/rocq-runtime/pretyping/combinators.cmi +lib/rocq-runtime/pretyping/combinators.cmt +lib/rocq-runtime/pretyping/combinators.cmti +lib/rocq-runtime/pretyping/combinators.cmx +lib/rocq-runtime/pretyping/combinators.ml +lib/rocq-runtime/pretyping/combinators.mli +lib/rocq-runtime/pretyping/constr_matching.cmi +lib/rocq-runtime/pretyping/constr_matching.cmt +lib/rocq-runtime/pretyping/constr_matching.cmti +lib/rocq-runtime/pretyping/constr_matching.cmx +lib/rocq-runtime/pretyping/constr_matching.ml +lib/rocq-runtime/pretyping/constr_matching.mli +lib/rocq-runtime/pretyping/detyping.cmi +lib/rocq-runtime/pretyping/detyping.cmt +lib/rocq-runtime/pretyping/detyping.cmti +lib/rocq-runtime/pretyping/detyping.cmx +lib/rocq-runtime/pretyping/detyping.ml +lib/rocq-runtime/pretyping/detyping.mli +lib/rocq-runtime/pretyping/evaluable.cmi +lib/rocq-runtime/pretyping/evaluable.cmt +lib/rocq-runtime/pretyping/evaluable.cmti +lib/rocq-runtime/pretyping/evaluable.cmx +lib/rocq-runtime/pretyping/evaluable.ml +lib/rocq-runtime/pretyping/evaluable.mli +lib/rocq-runtime/pretyping/evarconv.cmi +lib/rocq-runtime/pretyping/evarconv.cmt +lib/rocq-runtime/pretyping/evarconv.cmti +lib/rocq-runtime/pretyping/evarconv.cmx +lib/rocq-runtime/pretyping/evarconv.ml +lib/rocq-runtime/pretyping/evarconv.mli +lib/rocq-runtime/pretyping/evardefine.cmi +lib/rocq-runtime/pretyping/evardefine.cmt +lib/rocq-runtime/pretyping/evardefine.cmti +lib/rocq-runtime/pretyping/evardefine.cmx +lib/rocq-runtime/pretyping/evardefine.ml +lib/rocq-runtime/pretyping/evardefine.mli +lib/rocq-runtime/pretyping/evarsolve.cmi +lib/rocq-runtime/pretyping/evarsolve.cmt +lib/rocq-runtime/pretyping/evarsolve.cmti +lib/rocq-runtime/pretyping/evarsolve.cmx +lib/rocq-runtime/pretyping/evarsolve.ml +lib/rocq-runtime/pretyping/evarsolve.mli +lib/rocq-runtime/pretyping/find_subterm.cmi +lib/rocq-runtime/pretyping/find_subterm.cmt +lib/rocq-runtime/pretyping/find_subterm.cmti +lib/rocq-runtime/pretyping/find_subterm.cmx +lib/rocq-runtime/pretyping/find_subterm.ml +lib/rocq-runtime/pretyping/find_subterm.mli +lib/rocq-runtime/pretyping/genarg.cmi +lib/rocq-runtime/pretyping/genarg.cmt +lib/rocq-runtime/pretyping/genarg.cmti +lib/rocq-runtime/pretyping/genarg.cmx +lib/rocq-runtime/pretyping/genarg.ml +lib/rocq-runtime/pretyping/genarg.mli +lib/rocq-runtime/pretyping/geninterp.cmi +lib/rocq-runtime/pretyping/geninterp.cmt +lib/rocq-runtime/pretyping/geninterp.cmti +lib/rocq-runtime/pretyping/geninterp.cmx +lib/rocq-runtime/pretyping/geninterp.ml +lib/rocq-runtime/pretyping/geninterp.mli +lib/rocq-runtime/pretyping/gensubst.cmi +lib/rocq-runtime/pretyping/gensubst.cmt +lib/rocq-runtime/pretyping/gensubst.cmti +lib/rocq-runtime/pretyping/gensubst.cmx +lib/rocq-runtime/pretyping/gensubst.ml +lib/rocq-runtime/pretyping/gensubst.mli +lib/rocq-runtime/pretyping/globEnv.cmi +lib/rocq-runtime/pretyping/globEnv.cmt +lib/rocq-runtime/pretyping/globEnv.cmti +lib/rocq-runtime/pretyping/globEnv.cmx +lib/rocq-runtime/pretyping/globEnv.ml +lib/rocq-runtime/pretyping/globEnv.mli +lib/rocq-runtime/pretyping/glob_ops.cmi +lib/rocq-runtime/pretyping/glob_ops.cmt +lib/rocq-runtime/pretyping/glob_ops.cmti +lib/rocq-runtime/pretyping/glob_ops.cmx +lib/rocq-runtime/pretyping/glob_ops.ml +lib/rocq-runtime/pretyping/glob_ops.mli +lib/rocq-runtime/pretyping/glob_term.cmi +lib/rocq-runtime/pretyping/glob_term.cmti +lib/rocq-runtime/pretyping/glob_term.mli +lib/rocq-runtime/pretyping/heads.cmi +lib/rocq-runtime/pretyping/heads.cmt +lib/rocq-runtime/pretyping/heads.cmti +lib/rocq-runtime/pretyping/heads.cmx +lib/rocq-runtime/pretyping/heads.ml +lib/rocq-runtime/pretyping/heads.mli +lib/rocq-runtime/pretyping/indrec.cmi +lib/rocq-runtime/pretyping/indrec.cmt +lib/rocq-runtime/pretyping/indrec.cmti +lib/rocq-runtime/pretyping/indrec.cmx +lib/rocq-runtime/pretyping/indrec.ml +lib/rocq-runtime/pretyping/indrec.mli +lib/rocq-runtime/pretyping/inductiveops.cmi +lib/rocq-runtime/pretyping/inductiveops.cmt +lib/rocq-runtime/pretyping/inductiveops.cmti +lib/rocq-runtime/pretyping/inductiveops.cmx +lib/rocq-runtime/pretyping/inductiveops.ml +lib/rocq-runtime/pretyping/inductiveops.mli +lib/rocq-runtime/pretyping/keys.cmi +lib/rocq-runtime/pretyping/keys.cmt +lib/rocq-runtime/pretyping/keys.cmti +lib/rocq-runtime/pretyping/keys.cmx +lib/rocq-runtime/pretyping/keys.ml +lib/rocq-runtime/pretyping/keys.mli +lib/rocq-runtime/pretyping/locus.cmi +lib/rocq-runtime/pretyping/locus.cmti +lib/rocq-runtime/pretyping/locus.mli +lib/rocq-runtime/pretyping/locusops.cmi +lib/rocq-runtime/pretyping/locusops.cmt +lib/rocq-runtime/pretyping/locusops.cmti +lib/rocq-runtime/pretyping/locusops.cmx +lib/rocq-runtime/pretyping/locusops.ml +lib/rocq-runtime/pretyping/locusops.mli +lib/rocq-runtime/pretyping/ltac_pretype.cmi +lib/rocq-runtime/pretyping/ltac_pretype.cmti +lib/rocq-runtime/pretyping/ltac_pretype.mli +lib/rocq-runtime/pretyping/nativenorm.cmi +lib/rocq-runtime/pretyping/nativenorm.cmt +lib/rocq-runtime/pretyping/nativenorm.cmti +lib/rocq-runtime/pretyping/nativenorm.cmx +lib/rocq-runtime/pretyping/nativenorm.ml +lib/rocq-runtime/pretyping/nativenorm.mli +lib/rocq-runtime/pretyping/pattern.cmi +lib/rocq-runtime/pretyping/pattern.cmti +lib/rocq-runtime/pretyping/pattern.mli +lib/rocq-runtime/pretyping/patternops.cmi +lib/rocq-runtime/pretyping/patternops.cmt +lib/rocq-runtime/pretyping/patternops.cmti +lib/rocq-runtime/pretyping/patternops.cmx +lib/rocq-runtime/pretyping/patternops.ml +lib/rocq-runtime/pretyping/patternops.mli +lib/rocq-runtime/pretyping/pretype_errors.cmi +lib/rocq-runtime/pretyping/pretype_errors.cmt +lib/rocq-runtime/pretyping/pretype_errors.cmti +lib/rocq-runtime/pretyping/pretype_errors.cmx +lib/rocq-runtime/pretyping/pretype_errors.ml +lib/rocq-runtime/pretyping/pretype_errors.mli +lib/rocq-runtime/pretyping/pretyping.a +lib/rocq-runtime/pretyping/pretyping.cma +lib/rocq-runtime/pretyping/pretyping.cmi +lib/rocq-runtime/pretyping/pretyping.cmt +lib/rocq-runtime/pretyping/pretyping.cmti +lib/rocq-runtime/pretyping/pretyping.cmx +lib/rocq-runtime/pretyping/pretyping.cmxa +lib/rocq-runtime/pretyping/pretyping.cmxs +lib/rocq-runtime/pretyping/pretyping.ml +lib/rocq-runtime/pretyping/pretyping.mli +lib/rocq-runtime/pretyping/program.cmi +lib/rocq-runtime/pretyping/program.cmt +lib/rocq-runtime/pretyping/program.cmti +lib/rocq-runtime/pretyping/program.cmx +lib/rocq-runtime/pretyping/program.ml +lib/rocq-runtime/pretyping/program.mli +lib/rocq-runtime/pretyping/reductionops.cmi +lib/rocq-runtime/pretyping/reductionops.cmt +lib/rocq-runtime/pretyping/reductionops.cmti +lib/rocq-runtime/pretyping/reductionops.cmx +lib/rocq-runtime/pretyping/reductionops.ml +lib/rocq-runtime/pretyping/reductionops.mli +lib/rocq-runtime/pretyping/retyping.cmi +lib/rocq-runtime/pretyping/retyping.cmt +lib/rocq-runtime/pretyping/retyping.cmti +lib/rocq-runtime/pretyping/retyping.cmx +lib/rocq-runtime/pretyping/retyping.ml +lib/rocq-runtime/pretyping/retyping.mli +lib/rocq-runtime/pretyping/structures.cmi +lib/rocq-runtime/pretyping/structures.cmt +lib/rocq-runtime/pretyping/structures.cmti +lib/rocq-runtime/pretyping/structures.cmx +lib/rocq-runtime/pretyping/structures.ml +lib/rocq-runtime/pretyping/structures.mli +lib/rocq-runtime/pretyping/tacred.cmi +lib/rocq-runtime/pretyping/tacred.cmt +lib/rocq-runtime/pretyping/tacred.cmti +lib/rocq-runtime/pretyping/tacred.cmx +lib/rocq-runtime/pretyping/tacred.ml +lib/rocq-runtime/pretyping/tacred.mli +lib/rocq-runtime/pretyping/templateArity.cmi +lib/rocq-runtime/pretyping/templateArity.cmt +lib/rocq-runtime/pretyping/templateArity.cmti +lib/rocq-runtime/pretyping/templateArity.cmx +lib/rocq-runtime/pretyping/templateArity.ml +lib/rocq-runtime/pretyping/templateArity.mli +lib/rocq-runtime/pretyping/typeclasses.cmi +lib/rocq-runtime/pretyping/typeclasses.cmt +lib/rocq-runtime/pretyping/typeclasses.cmti +lib/rocq-runtime/pretyping/typeclasses.cmx +lib/rocq-runtime/pretyping/typeclasses.ml +lib/rocq-runtime/pretyping/typeclasses.mli +lib/rocq-runtime/pretyping/typeclasses_errors.cmi +lib/rocq-runtime/pretyping/typeclasses_errors.cmt +lib/rocq-runtime/pretyping/typeclasses_errors.cmti +lib/rocq-runtime/pretyping/typeclasses_errors.cmx +lib/rocq-runtime/pretyping/typeclasses_errors.ml +lib/rocq-runtime/pretyping/typeclasses_errors.mli +lib/rocq-runtime/pretyping/typing.cmi +lib/rocq-runtime/pretyping/typing.cmt +lib/rocq-runtime/pretyping/typing.cmti +lib/rocq-runtime/pretyping/typing.cmx +lib/rocq-runtime/pretyping/typing.ml +lib/rocq-runtime/pretyping/typing.mli +lib/rocq-runtime/pretyping/unification.cmi +lib/rocq-runtime/pretyping/unification.cmt +lib/rocq-runtime/pretyping/unification.cmti +lib/rocq-runtime/pretyping/unification.cmx +lib/rocq-runtime/pretyping/unification.ml +lib/rocq-runtime/pretyping/unification.mli +lib/rocq-runtime/pretyping/vnorm.cmi +lib/rocq-runtime/pretyping/vnorm.cmt +lib/rocq-runtime/pretyping/vnorm.cmti +lib/rocq-runtime/pretyping/vnorm.cmx +lib/rocq-runtime/pretyping/vnorm.ml +lib/rocq-runtime/pretyping/vnorm.mli +lib/rocq-runtime/printing/genprint.cmi +lib/rocq-runtime/printing/genprint.cmt +lib/rocq-runtime/printing/genprint.cmti +lib/rocq-runtime/printing/genprint.cmx +lib/rocq-runtime/printing/genprint.ml +lib/rocq-runtime/printing/genprint.mli +lib/rocq-runtime/printing/ppconstr.cmi +lib/rocq-runtime/printing/ppconstr.cmt +lib/rocq-runtime/printing/ppconstr.cmti +lib/rocq-runtime/printing/ppconstr.cmx +lib/rocq-runtime/printing/ppconstr.ml +lib/rocq-runtime/printing/ppconstr.mli +lib/rocq-runtime/printing/ppextend.cmi +lib/rocq-runtime/printing/ppextend.cmt +lib/rocq-runtime/printing/ppextend.cmti +lib/rocq-runtime/printing/ppextend.cmx +lib/rocq-runtime/printing/ppextend.ml +lib/rocq-runtime/printing/ppextend.mli +lib/rocq-runtime/printing/pputils.cmi +lib/rocq-runtime/printing/pputils.cmt +lib/rocq-runtime/printing/pputils.cmti +lib/rocq-runtime/printing/pputils.cmx +lib/rocq-runtime/printing/pputils.ml +lib/rocq-runtime/printing/pputils.mli +lib/rocq-runtime/printing/printer.cmi +lib/rocq-runtime/printing/printer.cmt +lib/rocq-runtime/printing/printer.cmti +lib/rocq-runtime/printing/printer.cmx +lib/rocq-runtime/printing/printer.ml +lib/rocq-runtime/printing/printer.mli +lib/rocq-runtime/printing/printing.a +lib/rocq-runtime/printing/printing.cma +lib/rocq-runtime/printing/printing.cmxa +lib/rocq-runtime/printing/printing.cmxs +lib/rocq-runtime/printing/proof_diffs.cmi +lib/rocq-runtime/printing/proof_diffs.cmt +lib/rocq-runtime/printing/proof_diffs.cmti +lib/rocq-runtime/printing/proof_diffs.cmx +lib/rocq-runtime/printing/proof_diffs.ml +lib/rocq-runtime/printing/proof_diffs.mli +lib/rocq-runtime/proofs/clenv.cmi +lib/rocq-runtime/proofs/clenv.cmt +lib/rocq-runtime/proofs/clenv.cmti +lib/rocq-runtime/proofs/clenv.cmx +lib/rocq-runtime/proofs/clenv.ml +lib/rocq-runtime/proofs/clenv.mli +lib/rocq-runtime/proofs/goal_select.cmi +lib/rocq-runtime/proofs/goal_select.cmt +lib/rocq-runtime/proofs/goal_select.cmti +lib/rocq-runtime/proofs/goal_select.cmx +lib/rocq-runtime/proofs/goal_select.ml +lib/rocq-runtime/proofs/goal_select.mli +lib/rocq-runtime/proofs/logic.cmi +lib/rocq-runtime/proofs/logic.cmt +lib/rocq-runtime/proofs/logic.cmti +lib/rocq-runtime/proofs/logic.cmx +lib/rocq-runtime/proofs/logic.ml +lib/rocq-runtime/proofs/logic.mli +lib/rocq-runtime/proofs/miscprint.cmi +lib/rocq-runtime/proofs/miscprint.cmt +lib/rocq-runtime/proofs/miscprint.cmti +lib/rocq-runtime/proofs/miscprint.cmx +lib/rocq-runtime/proofs/miscprint.ml +lib/rocq-runtime/proofs/miscprint.mli +lib/rocq-runtime/proofs/proof.cmi +lib/rocq-runtime/proofs/proof.cmt +lib/rocq-runtime/proofs/proof.cmti +lib/rocq-runtime/proofs/proof.cmx +lib/rocq-runtime/proofs/proof.ml +lib/rocq-runtime/proofs/proof.mli +lib/rocq-runtime/proofs/proof_bullet.cmi +lib/rocq-runtime/proofs/proof_bullet.cmt +lib/rocq-runtime/proofs/proof_bullet.cmti +lib/rocq-runtime/proofs/proof_bullet.cmx +lib/rocq-runtime/proofs/proof_bullet.ml +lib/rocq-runtime/proofs/proof_bullet.mli +lib/rocq-runtime/proofs/proofs.a +lib/rocq-runtime/proofs/proofs.cma +lib/rocq-runtime/proofs/proofs.cmxa +lib/rocq-runtime/proofs/proofs.cmxs +lib/rocq-runtime/proofs/refine.cmi +lib/rocq-runtime/proofs/refine.cmt +lib/rocq-runtime/proofs/refine.cmti +lib/rocq-runtime/proofs/refine.cmx +lib/rocq-runtime/proofs/refine.ml +lib/rocq-runtime/proofs/refine.mli +lib/rocq-runtime/proofs/tacmach.cmi +lib/rocq-runtime/proofs/tacmach.cmt +lib/rocq-runtime/proofs/tacmach.cmti +lib/rocq-runtime/proofs/tacmach.cmx +lib/rocq-runtime/proofs/tacmach.ml +lib/rocq-runtime/proofs/tacmach.mli +lib/rocq-runtime/proofs/tactypes.cmi +lib/rocq-runtime/proofs/tactypes.cmti +lib/rocq-runtime/proofs/tactypes.mli +lib/rocq-runtime/revision +lib/rocq-runtime/rocqnative +lib/rocq-runtime/rocqshim/rocqshim.a +lib/rocq-runtime/rocqshim/rocqshim.cma +lib/rocq-runtime/rocqshim/rocqshim.cmi +lib/rocq-runtime/rocqshim/rocqshim.cmt +lib/rocq-runtime/rocqshim/rocqshim.cmti +lib/rocq-runtime/rocqshim/rocqshim.cmx +lib/rocq-runtime/rocqshim/rocqshim.cmxa +lib/rocq-runtime/rocqshim/rocqshim.cmxs +lib/rocq-runtime/rocqshim/rocqshim.ml +lib/rocq-runtime/rocqshim/rocqshim.mli +lib/rocq-runtime/rocqworker +lib/rocq-runtime/rocqworker.byte +lib/rocq-runtime/rocqworker_with_drop +lib/rocq-runtime/stm/asyncTaskQueue.cmi +lib/rocq-runtime/stm/asyncTaskQueue.cmt +lib/rocq-runtime/stm/asyncTaskQueue.cmti +lib/rocq-runtime/stm/asyncTaskQueue.cmx +lib/rocq-runtime/stm/asyncTaskQueue.ml +lib/rocq-runtime/stm/asyncTaskQueue.mli +lib/rocq-runtime/stm/dag.cmi +lib/rocq-runtime/stm/dag.cmt +lib/rocq-runtime/stm/dag.cmti +lib/rocq-runtime/stm/dag.cmx +lib/rocq-runtime/stm/dag.ml +lib/rocq-runtime/stm/dag.mli +lib/rocq-runtime/stm/partac.cmi +lib/rocq-runtime/stm/partac.cmt +lib/rocq-runtime/stm/partac.cmti +lib/rocq-runtime/stm/partac.cmx +lib/rocq-runtime/stm/partac.ml +lib/rocq-runtime/stm/partac.mli +lib/rocq-runtime/stm/proofBlockDelimiter.cmi +lib/rocq-runtime/stm/proofBlockDelimiter.cmt +lib/rocq-runtime/stm/proofBlockDelimiter.cmti +lib/rocq-runtime/stm/proofBlockDelimiter.cmx +lib/rocq-runtime/stm/proofBlockDelimiter.ml +lib/rocq-runtime/stm/proofBlockDelimiter.mli +lib/rocq-runtime/stm/spawned.cmi +lib/rocq-runtime/stm/spawned.cmt +lib/rocq-runtime/stm/spawned.cmti +lib/rocq-runtime/stm/spawned.cmx +lib/rocq-runtime/stm/spawned.ml +lib/rocq-runtime/stm/spawned.mli +lib/rocq-runtime/stm/stm.a +lib/rocq-runtime/stm/stm.cma +lib/rocq-runtime/stm/stm.cmi +lib/rocq-runtime/stm/stm.cmt +lib/rocq-runtime/stm/stm.cmti +lib/rocq-runtime/stm/stm.cmx +lib/rocq-runtime/stm/stm.cmxa +lib/rocq-runtime/stm/stm.cmxs +lib/rocq-runtime/stm/stm.ml +lib/rocq-runtime/stm/stm.mli +lib/rocq-runtime/stm/stmargs.cmi +lib/rocq-runtime/stm/stmargs.cmt +lib/rocq-runtime/stm/stmargs.cmti +lib/rocq-runtime/stm/stmargs.cmx +lib/rocq-runtime/stm/stmargs.ml +lib/rocq-runtime/stm/stmargs.mli +lib/rocq-runtime/stm/tQueue.cmi +lib/rocq-runtime/stm/tQueue.cmt +lib/rocq-runtime/stm/tQueue.cmti +lib/rocq-runtime/stm/tQueue.cmx +lib/rocq-runtime/stm/tQueue.ml +lib/rocq-runtime/stm/tQueue.mli +lib/rocq-runtime/stm/vcs.cmi +lib/rocq-runtime/stm/vcs.cmt +lib/rocq-runtime/stm/vcs.cmti +lib/rocq-runtime/stm/vcs.cmx +lib/rocq-runtime/stm/vcs.ml +lib/rocq-runtime/stm/vcs.mli +lib/rocq-runtime/stm/workerPool.cmi +lib/rocq-runtime/stm/workerPool.cmt +lib/rocq-runtime/stm/workerPool.cmti +lib/rocq-runtime/stm/workerPool.cmx +lib/rocq-runtime/stm/workerPool.ml +lib/rocq-runtime/stm/workerPool.mli +lib/rocq-runtime/sysinit/coqinit.cmi +lib/rocq-runtime/sysinit/coqinit.cmt +lib/rocq-runtime/sysinit/coqinit.cmti +lib/rocq-runtime/sysinit/coqinit.cmx +lib/rocq-runtime/sysinit/coqinit.ml +lib/rocq-runtime/sysinit/coqinit.mli +lib/rocq-runtime/sysinit/coqloadpath.cmi +lib/rocq-runtime/sysinit/coqloadpath.cmt +lib/rocq-runtime/sysinit/coqloadpath.cmti +lib/rocq-runtime/sysinit/coqloadpath.cmx +lib/rocq-runtime/sysinit/coqloadpath.ml +lib/rocq-runtime/sysinit/coqloadpath.mli +lib/rocq-runtime/sysinit/sysinit.a +lib/rocq-runtime/sysinit/sysinit.cma +lib/rocq-runtime/sysinit/sysinit.cmxa +lib/rocq-runtime/sysinit/sysinit.cmxs +lib/rocq-runtime/tactics/abstract.cmi +lib/rocq-runtime/tactics/abstract.cmt +lib/rocq-runtime/tactics/abstract.cmti +lib/rocq-runtime/tactics/abstract.cmx +lib/rocq-runtime/tactics/abstract.ml +lib/rocq-runtime/tactics/abstract.mli +lib/rocq-runtime/tactics/auto.cmi +lib/rocq-runtime/tactics/auto.cmt +lib/rocq-runtime/tactics/auto.cmti +lib/rocq-runtime/tactics/auto.cmx +lib/rocq-runtime/tactics/auto.ml +lib/rocq-runtime/tactics/auto.mli +lib/rocq-runtime/tactics/autorewrite.cmi +lib/rocq-runtime/tactics/autorewrite.cmt +lib/rocq-runtime/tactics/autorewrite.cmti +lib/rocq-runtime/tactics/autorewrite.cmx +lib/rocq-runtime/tactics/autorewrite.ml +lib/rocq-runtime/tactics/autorewrite.mli +lib/rocq-runtime/tactics/btermdn.cmi +lib/rocq-runtime/tactics/btermdn.cmt +lib/rocq-runtime/tactics/btermdn.cmti +lib/rocq-runtime/tactics/btermdn.cmx +lib/rocq-runtime/tactics/btermdn.ml +lib/rocq-runtime/tactics/btermdn.mli +lib/rocq-runtime/tactics/cbn.cmi +lib/rocq-runtime/tactics/cbn.cmt +lib/rocq-runtime/tactics/cbn.cmti +lib/rocq-runtime/tactics/cbn.cmx +lib/rocq-runtime/tactics/cbn.ml +lib/rocq-runtime/tactics/cbn.mli +lib/rocq-runtime/tactics/class_tactics.cmi +lib/rocq-runtime/tactics/class_tactics.cmt +lib/rocq-runtime/tactics/class_tactics.cmti +lib/rocq-runtime/tactics/class_tactics.cmx +lib/rocq-runtime/tactics/class_tactics.ml +lib/rocq-runtime/tactics/class_tactics.mli +lib/rocq-runtime/tactics/contradiction.cmi +lib/rocq-runtime/tactics/contradiction.cmt +lib/rocq-runtime/tactics/contradiction.cmti +lib/rocq-runtime/tactics/contradiction.cmx +lib/rocq-runtime/tactics/contradiction.ml +lib/rocq-runtime/tactics/contradiction.mli +lib/rocq-runtime/tactics/declareScheme.cmi +lib/rocq-runtime/tactics/declareScheme.cmt +lib/rocq-runtime/tactics/declareScheme.cmti +lib/rocq-runtime/tactics/declareScheme.cmx +lib/rocq-runtime/tactics/declareScheme.ml +lib/rocq-runtime/tactics/declareScheme.mli +lib/rocq-runtime/tactics/dn.cmi +lib/rocq-runtime/tactics/dn.cmt +lib/rocq-runtime/tactics/dn.cmti +lib/rocq-runtime/tactics/dn.cmx +lib/rocq-runtime/tactics/dn.ml +lib/rocq-runtime/tactics/dn.mli +lib/rocq-runtime/tactics/eClause.cmi +lib/rocq-runtime/tactics/eClause.cmt +lib/rocq-runtime/tactics/eClause.cmti +lib/rocq-runtime/tactics/eClause.cmx +lib/rocq-runtime/tactics/eClause.ml +lib/rocq-runtime/tactics/eClause.mli +lib/rocq-runtime/tactics/eauto.cmi +lib/rocq-runtime/tactics/eauto.cmt +lib/rocq-runtime/tactics/eauto.cmti +lib/rocq-runtime/tactics/eauto.cmx +lib/rocq-runtime/tactics/eauto.ml +lib/rocq-runtime/tactics/eauto.mli +lib/rocq-runtime/tactics/elim.cmi +lib/rocq-runtime/tactics/elim.cmt +lib/rocq-runtime/tactics/elim.cmti +lib/rocq-runtime/tactics/elim.cmx +lib/rocq-runtime/tactics/elim.ml +lib/rocq-runtime/tactics/elim.mli +lib/rocq-runtime/tactics/elimschemes.cmi +lib/rocq-runtime/tactics/elimschemes.cmt +lib/rocq-runtime/tactics/elimschemes.cmti +lib/rocq-runtime/tactics/elimschemes.cmx +lib/rocq-runtime/tactics/elimschemes.ml +lib/rocq-runtime/tactics/elimschemes.mli +lib/rocq-runtime/tactics/eqdecide.cmi +lib/rocq-runtime/tactics/eqdecide.cmt +lib/rocq-runtime/tactics/eqdecide.cmti +lib/rocq-runtime/tactics/eqdecide.cmx +lib/rocq-runtime/tactics/eqdecide.ml +lib/rocq-runtime/tactics/eqdecide.mli +lib/rocq-runtime/tactics/eqschemes.cmi +lib/rocq-runtime/tactics/eqschemes.cmt +lib/rocq-runtime/tactics/eqschemes.cmti +lib/rocq-runtime/tactics/eqschemes.cmx +lib/rocq-runtime/tactics/eqschemes.ml +lib/rocq-runtime/tactics/eqschemes.mli +lib/rocq-runtime/tactics/equality.cmi +lib/rocq-runtime/tactics/equality.cmt +lib/rocq-runtime/tactics/equality.cmti +lib/rocq-runtime/tactics/equality.cmx +lib/rocq-runtime/tactics/equality.ml +lib/rocq-runtime/tactics/equality.mli +lib/rocq-runtime/tactics/evar_tactics.cmi +lib/rocq-runtime/tactics/evar_tactics.cmt +lib/rocq-runtime/tactics/evar_tactics.cmti +lib/rocq-runtime/tactics/evar_tactics.cmx +lib/rocq-runtime/tactics/evar_tactics.ml +lib/rocq-runtime/tactics/evar_tactics.mli +lib/rocq-runtime/tactics/generalize.cmi +lib/rocq-runtime/tactics/generalize.cmt +lib/rocq-runtime/tactics/generalize.cmti +lib/rocq-runtime/tactics/generalize.cmx +lib/rocq-runtime/tactics/generalize.ml +lib/rocq-runtime/tactics/generalize.mli +lib/rocq-runtime/tactics/genredexpr.cmi +lib/rocq-runtime/tactics/genredexpr.cmti +lib/rocq-runtime/tactics/genredexpr.mli +lib/rocq-runtime/tactics/gentactic.cmi +lib/rocq-runtime/tactics/gentactic.cmt +lib/rocq-runtime/tactics/gentactic.cmti +lib/rocq-runtime/tactics/gentactic.cmx +lib/rocq-runtime/tactics/gentactic.ml +lib/rocq-runtime/tactics/gentactic.mli +lib/rocq-runtime/tactics/hints.cmi +lib/rocq-runtime/tactics/hints.cmt +lib/rocq-runtime/tactics/hints.cmti +lib/rocq-runtime/tactics/hints.cmx +lib/rocq-runtime/tactics/hints.ml +lib/rocq-runtime/tactics/hints.mli +lib/rocq-runtime/tactics/hipattern.cmi +lib/rocq-runtime/tactics/hipattern.cmt +lib/rocq-runtime/tactics/hipattern.cmti +lib/rocq-runtime/tactics/hipattern.cmx +lib/rocq-runtime/tactics/hipattern.ml +lib/rocq-runtime/tactics/hipattern.mli +lib/rocq-runtime/tactics/ind_tables.cmi +lib/rocq-runtime/tactics/ind_tables.cmt +lib/rocq-runtime/tactics/ind_tables.cmti +lib/rocq-runtime/tactics/ind_tables.cmx +lib/rocq-runtime/tactics/ind_tables.ml +lib/rocq-runtime/tactics/ind_tables.mli +lib/rocq-runtime/tactics/induction.cmi +lib/rocq-runtime/tactics/induction.cmt +lib/rocq-runtime/tactics/induction.cmti +lib/rocq-runtime/tactics/induction.cmx +lib/rocq-runtime/tactics/induction.ml +lib/rocq-runtime/tactics/induction.mli +lib/rocq-runtime/tactics/inv.cmi +lib/rocq-runtime/tactics/inv.cmt +lib/rocq-runtime/tactics/inv.cmti +lib/rocq-runtime/tactics/inv.cmx +lib/rocq-runtime/tactics/inv.ml +lib/rocq-runtime/tactics/inv.mli +lib/rocq-runtime/tactics/ppred.cmi +lib/rocq-runtime/tactics/ppred.cmt +lib/rocq-runtime/tactics/ppred.cmti +lib/rocq-runtime/tactics/ppred.cmx +lib/rocq-runtime/tactics/ppred.ml +lib/rocq-runtime/tactics/ppred.mli +lib/rocq-runtime/tactics/redexpr.cmi +lib/rocq-runtime/tactics/redexpr.cmt +lib/rocq-runtime/tactics/redexpr.cmti +lib/rocq-runtime/tactics/redexpr.cmx +lib/rocq-runtime/tactics/redexpr.ml +lib/rocq-runtime/tactics/redexpr.mli +lib/rocq-runtime/tactics/redops.cmi +lib/rocq-runtime/tactics/redops.cmt +lib/rocq-runtime/tactics/redops.cmti +lib/rocq-runtime/tactics/redops.cmx +lib/rocq-runtime/tactics/redops.ml +lib/rocq-runtime/tactics/redops.mli +lib/rocq-runtime/tactics/rewrite.cmi +lib/rocq-runtime/tactics/rewrite.cmt +lib/rocq-runtime/tactics/rewrite.cmti +lib/rocq-runtime/tactics/rewrite.cmx +lib/rocq-runtime/tactics/rewrite.ml +lib/rocq-runtime/tactics/rewrite.mli +lib/rocq-runtime/tactics/stdarg.cmi +lib/rocq-runtime/tactics/stdarg.cmt +lib/rocq-runtime/tactics/stdarg.cmti +lib/rocq-runtime/tactics/stdarg.cmx +lib/rocq-runtime/tactics/stdarg.ml +lib/rocq-runtime/tactics/stdarg.mli +lib/rocq-runtime/tactics/tacticals.cmi +lib/rocq-runtime/tactics/tacticals.cmt +lib/rocq-runtime/tactics/tacticals.cmti +lib/rocq-runtime/tactics/tacticals.cmx +lib/rocq-runtime/tactics/tacticals.ml +lib/rocq-runtime/tactics/tacticals.mli +lib/rocq-runtime/tactics/tactics.a +lib/rocq-runtime/tactics/tactics.cma +lib/rocq-runtime/tactics/tactics.cmi +lib/rocq-runtime/tactics/tactics.cmt +lib/rocq-runtime/tactics/tactics.cmti +lib/rocq-runtime/tactics/tactics.cmx +lib/rocq-runtime/tactics/tactics.cmxa +lib/rocq-runtime/tactics/tactics.cmxs +lib/rocq-runtime/tactics/tactics.ml +lib/rocq-runtime/tactics/tactics.mli +lib/rocq-runtime/tools/CoqMakefile.in +lib/rocq-runtime/tools/TimeFileMaker.py +lib/rocq-runtime/tools/coqdoc/coqdoc.css +lib/rocq-runtime/tools/coqdoc/coqdoc.sty +lib/rocq-runtime/tools/make-both-single-timing-files.py +lib/rocq-runtime/tools/make-both-time-files.py +lib/rocq-runtime/tools/make-one-time-file.py +lib/rocq-runtime/toplevel/ccompile.cmi +lib/rocq-runtime/toplevel/ccompile.cmt +lib/rocq-runtime/toplevel/ccompile.cmti +lib/rocq-runtime/toplevel/ccompile.cmx +lib/rocq-runtime/toplevel/ccompile.ml +lib/rocq-runtime/toplevel/ccompile.mli +lib/rocq-runtime/toplevel/colors.cmi +lib/rocq-runtime/toplevel/colors.cmt +lib/rocq-runtime/toplevel/colors.cmti +lib/rocq-runtime/toplevel/colors.cmx +lib/rocq-runtime/toplevel/colors.ml +lib/rocq-runtime/toplevel/colors.mli +lib/rocq-runtime/toplevel/common_compile.cmi +lib/rocq-runtime/toplevel/common_compile.cmt +lib/rocq-runtime/toplevel/common_compile.cmti +lib/rocq-runtime/toplevel/common_compile.cmx +lib/rocq-runtime/toplevel/common_compile.ml +lib/rocq-runtime/toplevel/common_compile.mli +lib/rocq-runtime/toplevel/coqc.cmi +lib/rocq-runtime/toplevel/coqc.cmt +lib/rocq-runtime/toplevel/coqc.cmti +lib/rocq-runtime/toplevel/coqc.cmx +lib/rocq-runtime/toplevel/coqc.ml +lib/rocq-runtime/toplevel/coqc.mli +lib/rocq-runtime/toplevel/coqcargs.cmi +lib/rocq-runtime/toplevel/coqcargs.cmt +lib/rocq-runtime/toplevel/coqcargs.cmti +lib/rocq-runtime/toplevel/coqcargs.cmx +lib/rocq-runtime/toplevel/coqcargs.ml +lib/rocq-runtime/toplevel/coqcargs.mli +lib/rocq-runtime/toplevel/coqloop.cmi +lib/rocq-runtime/toplevel/coqloop.cmt +lib/rocq-runtime/toplevel/coqloop.cmti +lib/rocq-runtime/toplevel/coqloop.cmx +lib/rocq-runtime/toplevel/coqloop.ml +lib/rocq-runtime/toplevel/coqloop.mli +lib/rocq-runtime/toplevel/coqrc.cmi +lib/rocq-runtime/toplevel/coqrc.cmt +lib/rocq-runtime/toplevel/coqrc.cmti +lib/rocq-runtime/toplevel/coqrc.cmx +lib/rocq-runtime/toplevel/coqrc.ml +lib/rocq-runtime/toplevel/coqrc.mli +lib/rocq-runtime/toplevel/coqtop.cmi +lib/rocq-runtime/toplevel/coqtop.cmt +lib/rocq-runtime/toplevel/coqtop.cmti +lib/rocq-runtime/toplevel/coqtop.cmx +lib/rocq-runtime/toplevel/coqtop.ml +lib/rocq-runtime/toplevel/coqtop.mli +lib/rocq-runtime/toplevel/g_toplevel.cmi +lib/rocq-runtime/toplevel/g_toplevel.cmt +lib/rocq-runtime/toplevel/g_toplevel.cmti +lib/rocq-runtime/toplevel/g_toplevel.cmx +lib/rocq-runtime/toplevel/g_toplevel.ml +lib/rocq-runtime/toplevel/g_toplevel.mli +lib/rocq-runtime/toplevel/load.cmi +lib/rocq-runtime/toplevel/load.cmt +lib/rocq-runtime/toplevel/load.cmti +lib/rocq-runtime/toplevel/load.cmx +lib/rocq-runtime/toplevel/load.ml +lib/rocq-runtime/toplevel/load.mli +lib/rocq-runtime/toplevel/memtrace_init.cmi +lib/rocq-runtime/toplevel/memtrace_init.cmt +lib/rocq-runtime/toplevel/memtrace_init.cmti +lib/rocq-runtime/toplevel/memtrace_init.cmx +lib/rocq-runtime/toplevel/memtrace_init.ml +lib/rocq-runtime/toplevel/memtrace_init.mli +lib/rocq-runtime/toplevel/toplevel.a +lib/rocq-runtime/toplevel/toplevel.cma +lib/rocq-runtime/toplevel/toplevel.cmxa +lib/rocq-runtime/toplevel/toplevel.cmxs +lib/rocq-runtime/toplevel/vernac.cmi +lib/rocq-runtime/toplevel/vernac.cmt +lib/rocq-runtime/toplevel/vernac.cmti +lib/rocq-runtime/toplevel/vernac.cmx +lib/rocq-runtime/toplevel/vernac.ml +lib/rocq-runtime/toplevel/vernac.mli +lib/rocq-runtime/toplevel/workerLoop.cmi +lib/rocq-runtime/toplevel/workerLoop.cmt +lib/rocq-runtime/toplevel/workerLoop.cmti +lib/rocq-runtime/toplevel/workerLoop.cmx +lib/rocq-runtime/toplevel/workerLoop.ml +lib/rocq-runtime/toplevel/workerLoop.mli +lib/rocq-runtime/vernac/assumptions.cmi +lib/rocq-runtime/vernac/assumptions.cmt +lib/rocq-runtime/vernac/assumptions.cmti +lib/rocq-runtime/vernac/assumptions.cmx +lib/rocq-runtime/vernac/assumptions.ml +lib/rocq-runtime/vernac/assumptions.mli +lib/rocq-runtime/vernac/attributes.cmi +lib/rocq-runtime/vernac/attributes.cmt +lib/rocq-runtime/vernac/attributes.cmti +lib/rocq-runtime/vernac/attributes.cmx +lib/rocq-runtime/vernac/attributes.ml +lib/rocq-runtime/vernac/attributes.mli +lib/rocq-runtime/vernac/auto_ind_decl.cmi +lib/rocq-runtime/vernac/auto_ind_decl.cmt +lib/rocq-runtime/vernac/auto_ind_decl.cmti +lib/rocq-runtime/vernac/auto_ind_decl.cmx +lib/rocq-runtime/vernac/auto_ind_decl.ml +lib/rocq-runtime/vernac/auto_ind_decl.mli +lib/rocq-runtime/vernac/canonical.cmi +lib/rocq-runtime/vernac/canonical.cmt +lib/rocq-runtime/vernac/canonical.cmti +lib/rocq-runtime/vernac/canonical.cmx +lib/rocq-runtime/vernac/canonical.ml +lib/rocq-runtime/vernac/canonical.mli +lib/rocq-runtime/vernac/classes.cmi +lib/rocq-runtime/vernac/classes.cmt +lib/rocq-runtime/vernac/classes.cmti +lib/rocq-runtime/vernac/classes.cmx +lib/rocq-runtime/vernac/classes.ml +lib/rocq-runtime/vernac/classes.mli +lib/rocq-runtime/vernac/comArguments.cmi +lib/rocq-runtime/vernac/comArguments.cmt +lib/rocq-runtime/vernac/comArguments.cmti +lib/rocq-runtime/vernac/comArguments.cmx +lib/rocq-runtime/vernac/comArguments.ml +lib/rocq-runtime/vernac/comArguments.mli +lib/rocq-runtime/vernac/comAssumption.cmi +lib/rocq-runtime/vernac/comAssumption.cmt +lib/rocq-runtime/vernac/comAssumption.cmti +lib/rocq-runtime/vernac/comAssumption.cmx +lib/rocq-runtime/vernac/comAssumption.ml +lib/rocq-runtime/vernac/comAssumption.mli +lib/rocq-runtime/vernac/comCoercion.cmi +lib/rocq-runtime/vernac/comCoercion.cmt +lib/rocq-runtime/vernac/comCoercion.cmti +lib/rocq-runtime/vernac/comCoercion.cmx +lib/rocq-runtime/vernac/comCoercion.ml +lib/rocq-runtime/vernac/comCoercion.mli +lib/rocq-runtime/vernac/comDefinition.cmi +lib/rocq-runtime/vernac/comDefinition.cmt +lib/rocq-runtime/vernac/comDefinition.cmti +lib/rocq-runtime/vernac/comDefinition.cmx +lib/rocq-runtime/vernac/comDefinition.ml +lib/rocq-runtime/vernac/comDefinition.mli +lib/rocq-runtime/vernac/comExtraDeps.cmi +lib/rocq-runtime/vernac/comExtraDeps.cmt +lib/rocq-runtime/vernac/comExtraDeps.cmti +lib/rocq-runtime/vernac/comExtraDeps.cmx +lib/rocq-runtime/vernac/comExtraDeps.ml +lib/rocq-runtime/vernac/comExtraDeps.mli +lib/rocq-runtime/vernac/comFixpoint.cmi +lib/rocq-runtime/vernac/comFixpoint.cmt +lib/rocq-runtime/vernac/comFixpoint.cmti +lib/rocq-runtime/vernac/comFixpoint.cmx +lib/rocq-runtime/vernac/comFixpoint.ml +lib/rocq-runtime/vernac/comFixpoint.mli +lib/rocq-runtime/vernac/comHints.cmi +lib/rocq-runtime/vernac/comHints.cmt +lib/rocq-runtime/vernac/comHints.cmti +lib/rocq-runtime/vernac/comHints.cmx +lib/rocq-runtime/vernac/comHints.ml +lib/rocq-runtime/vernac/comHints.mli +lib/rocq-runtime/vernac/comInductive.cmi +lib/rocq-runtime/vernac/comInductive.cmt +lib/rocq-runtime/vernac/comInductive.cmti +lib/rocq-runtime/vernac/comInductive.cmx +lib/rocq-runtime/vernac/comInductive.ml +lib/rocq-runtime/vernac/comInductive.mli +lib/rocq-runtime/vernac/comPrimitive.cmi +lib/rocq-runtime/vernac/comPrimitive.cmt +lib/rocq-runtime/vernac/comPrimitive.cmti +lib/rocq-runtime/vernac/comPrimitive.cmx +lib/rocq-runtime/vernac/comPrimitive.ml +lib/rocq-runtime/vernac/comPrimitive.mli +lib/rocq-runtime/vernac/comRewriteRule.cmi +lib/rocq-runtime/vernac/comRewriteRule.cmt +lib/rocq-runtime/vernac/comRewriteRule.cmti +lib/rocq-runtime/vernac/comRewriteRule.cmx +lib/rocq-runtime/vernac/comRewriteRule.ml +lib/rocq-runtime/vernac/comRewriteRule.mli +lib/rocq-runtime/vernac/comSearch.cmi +lib/rocq-runtime/vernac/comSearch.cmt +lib/rocq-runtime/vernac/comSearch.cmti +lib/rocq-runtime/vernac/comSearch.cmx +lib/rocq-runtime/vernac/comSearch.ml +lib/rocq-runtime/vernac/comSearch.mli +lib/rocq-runtime/vernac/comTactic.cmi +lib/rocq-runtime/vernac/comTactic.cmt +lib/rocq-runtime/vernac/comTactic.cmti +lib/rocq-runtime/vernac/comTactic.cmx +lib/rocq-runtime/vernac/comTactic.ml +lib/rocq-runtime/vernac/comTactic.mli +lib/rocq-runtime/vernac/debugHook.cmi +lib/rocq-runtime/vernac/debugHook.cmt +lib/rocq-runtime/vernac/debugHook.cmti +lib/rocq-runtime/vernac/debugHook.cmx +lib/rocq-runtime/vernac/debugHook.ml +lib/rocq-runtime/vernac/debugHook.mli +lib/rocq-runtime/vernac/declare.cmi +lib/rocq-runtime/vernac/declare.cmt +lib/rocq-runtime/vernac/declare.cmti +lib/rocq-runtime/vernac/declare.cmx +lib/rocq-runtime/vernac/declare.ml +lib/rocq-runtime/vernac/declare.mli +lib/rocq-runtime/vernac/declareInd.cmi +lib/rocq-runtime/vernac/declareInd.cmt +lib/rocq-runtime/vernac/declareInd.cmti +lib/rocq-runtime/vernac/declareInd.cmx +lib/rocq-runtime/vernac/declareInd.ml +lib/rocq-runtime/vernac/declareInd.mli +lib/rocq-runtime/vernac/declareUniv.cmi +lib/rocq-runtime/vernac/declareUniv.cmt +lib/rocq-runtime/vernac/declareUniv.cmti +lib/rocq-runtime/vernac/declareUniv.cmx +lib/rocq-runtime/vernac/declareUniv.ml +lib/rocq-runtime/vernac/declareUniv.mli +lib/rocq-runtime/vernac/declaremods.cmi +lib/rocq-runtime/vernac/declaremods.cmt +lib/rocq-runtime/vernac/declaremods.cmti +lib/rocq-runtime/vernac/declaremods.cmx +lib/rocq-runtime/vernac/declaremods.ml +lib/rocq-runtime/vernac/declaremods.mli +lib/rocq-runtime/vernac/egramml.cmi +lib/rocq-runtime/vernac/egramml.cmt +lib/rocq-runtime/vernac/egramml.cmti +lib/rocq-runtime/vernac/egramml.cmx +lib/rocq-runtime/vernac/egramml.ml +lib/rocq-runtime/vernac/egramml.mli +lib/rocq-runtime/vernac/egramrocq.cmi +lib/rocq-runtime/vernac/egramrocq.cmt +lib/rocq-runtime/vernac/egramrocq.cmti +lib/rocq-runtime/vernac/egramrocq.cmx +lib/rocq-runtime/vernac/egramrocq.ml +lib/rocq-runtime/vernac/egramrocq.mli +lib/rocq-runtime/vernac/future.cmi +lib/rocq-runtime/vernac/future.cmt +lib/rocq-runtime/vernac/future.cmti +lib/rocq-runtime/vernac/future.cmx +lib/rocq-runtime/vernac/future.ml +lib/rocq-runtime/vernac/future.mli +lib/rocq-runtime/vernac/g_obligations.cmi +lib/rocq-runtime/vernac/g_obligations.cmt +lib/rocq-runtime/vernac/g_obligations.cmti +lib/rocq-runtime/vernac/g_obligations.cmx +lib/rocq-runtime/vernac/g_obligations.ml +lib/rocq-runtime/vernac/g_obligations.mli +lib/rocq-runtime/vernac/g_proofs.cmi +lib/rocq-runtime/vernac/g_proofs.cmt +lib/rocq-runtime/vernac/g_proofs.cmti +lib/rocq-runtime/vernac/g_proofs.cmx +lib/rocq-runtime/vernac/g_proofs.ml +lib/rocq-runtime/vernac/g_proofs.mli +lib/rocq-runtime/vernac/g_redexpr.cmi +lib/rocq-runtime/vernac/g_redexpr.cmt +lib/rocq-runtime/vernac/g_redexpr.cmti +lib/rocq-runtime/vernac/g_redexpr.cmx +lib/rocq-runtime/vernac/g_redexpr.ml +lib/rocq-runtime/vernac/g_redexpr.mli +lib/rocq-runtime/vernac/g_vernac.cmi +lib/rocq-runtime/vernac/g_vernac.cmt +lib/rocq-runtime/vernac/g_vernac.cmti +lib/rocq-runtime/vernac/g_vernac.cmx +lib/rocq-runtime/vernac/g_vernac.ml +lib/rocq-runtime/vernac/g_vernac.mli +lib/rocq-runtime/vernac/himsg.cmi +lib/rocq-runtime/vernac/himsg.cmt +lib/rocq-runtime/vernac/himsg.cmti +lib/rocq-runtime/vernac/himsg.cmx +lib/rocq-runtime/vernac/himsg.ml +lib/rocq-runtime/vernac/himsg.mli +lib/rocq-runtime/vernac/indschemes.cmi +lib/rocq-runtime/vernac/indschemes.cmt +lib/rocq-runtime/vernac/indschemes.cmti +lib/rocq-runtime/vernac/indschemes.cmx +lib/rocq-runtime/vernac/indschemes.ml +lib/rocq-runtime/vernac/indschemes.mli +lib/rocq-runtime/vernac/library.cmi +lib/rocq-runtime/vernac/library.cmt +lib/rocq-runtime/vernac/library.cmti +lib/rocq-runtime/vernac/library.cmx +lib/rocq-runtime/vernac/library.ml +lib/rocq-runtime/vernac/library.mli +lib/rocq-runtime/vernac/loadpath.cmi +lib/rocq-runtime/vernac/loadpath.cmt +lib/rocq-runtime/vernac/loadpath.cmti +lib/rocq-runtime/vernac/loadpath.cmx +lib/rocq-runtime/vernac/loadpath.ml +lib/rocq-runtime/vernac/loadpath.mli +lib/rocq-runtime/vernac/metasyntax.cmi +lib/rocq-runtime/vernac/metasyntax.cmt +lib/rocq-runtime/vernac/metasyntax.cmti +lib/rocq-runtime/vernac/metasyntax.cmx +lib/rocq-runtime/vernac/metasyntax.ml +lib/rocq-runtime/vernac/metasyntax.mli +lib/rocq-runtime/vernac/mltop.cmi +lib/rocq-runtime/vernac/mltop.cmt +lib/rocq-runtime/vernac/mltop.cmti +lib/rocq-runtime/vernac/mltop.cmx +lib/rocq-runtime/vernac/mltop.ml +lib/rocq-runtime/vernac/mltop.mli +lib/rocq-runtime/vernac/opaques.cmi +lib/rocq-runtime/vernac/opaques.cmt +lib/rocq-runtime/vernac/opaques.cmti +lib/rocq-runtime/vernac/opaques.cmx +lib/rocq-runtime/vernac/opaques.ml +lib/rocq-runtime/vernac/opaques.mli +lib/rocq-runtime/vernac/ppvernac.cmi +lib/rocq-runtime/vernac/ppvernac.cmt +lib/rocq-runtime/vernac/ppvernac.cmti +lib/rocq-runtime/vernac/ppvernac.cmx +lib/rocq-runtime/vernac/ppvernac.ml +lib/rocq-runtime/vernac/ppvernac.mli +lib/rocq-runtime/vernac/prettyp.cmi +lib/rocq-runtime/vernac/prettyp.cmt +lib/rocq-runtime/vernac/prettyp.cmti +lib/rocq-runtime/vernac/prettyp.cmx +lib/rocq-runtime/vernac/prettyp.ml +lib/rocq-runtime/vernac/prettyp.mli +lib/rocq-runtime/vernac/printmod.cmi +lib/rocq-runtime/vernac/printmod.cmt +lib/rocq-runtime/vernac/printmod.cmti +lib/rocq-runtime/vernac/printmod.cmx +lib/rocq-runtime/vernac/printmod.ml +lib/rocq-runtime/vernac/printmod.mli +lib/rocq-runtime/vernac/proof_using.cmi +lib/rocq-runtime/vernac/proof_using.cmt +lib/rocq-runtime/vernac/proof_using.cmti +lib/rocq-runtime/vernac/proof_using.cmx +lib/rocq-runtime/vernac/proof_using.ml +lib/rocq-runtime/vernac/proof_using.mli +lib/rocq-runtime/vernac/pvernac.cmi +lib/rocq-runtime/vernac/pvernac.cmt +lib/rocq-runtime/vernac/pvernac.cmti +lib/rocq-runtime/vernac/pvernac.cmx +lib/rocq-runtime/vernac/pvernac.ml +lib/rocq-runtime/vernac/pvernac.mli +lib/rocq-runtime/vernac/recLemmas.cmi +lib/rocq-runtime/vernac/recLemmas.cmt +lib/rocq-runtime/vernac/recLemmas.cmti +lib/rocq-runtime/vernac/recLemmas.cmx +lib/rocq-runtime/vernac/recLemmas.ml +lib/rocq-runtime/vernac/recLemmas.mli +lib/rocq-runtime/vernac/record.cmi +lib/rocq-runtime/vernac/record.cmt +lib/rocq-runtime/vernac/record.cmti +lib/rocq-runtime/vernac/record.cmx +lib/rocq-runtime/vernac/record.ml +lib/rocq-runtime/vernac/record.mli +lib/rocq-runtime/vernac/retrieveObl.cmi +lib/rocq-runtime/vernac/retrieveObl.cmt +lib/rocq-runtime/vernac/retrieveObl.cmti +lib/rocq-runtime/vernac/retrieveObl.cmx +lib/rocq-runtime/vernac/retrieveObl.ml +lib/rocq-runtime/vernac/retrieveObl.mli +lib/rocq-runtime/vernac/search.cmi +lib/rocq-runtime/vernac/search.cmt +lib/rocq-runtime/vernac/search.cmti +lib/rocq-runtime/vernac/search.cmx +lib/rocq-runtime/vernac/search.ml +lib/rocq-runtime/vernac/search.mli +lib/rocq-runtime/vernac/synterp.cmi +lib/rocq-runtime/vernac/synterp.cmt +lib/rocq-runtime/vernac/synterp.cmti +lib/rocq-runtime/vernac/synterp.cmx +lib/rocq-runtime/vernac/synterp.ml +lib/rocq-runtime/vernac/synterp.mli +lib/rocq-runtime/vernac/tactic_option.cmi +lib/rocq-runtime/vernac/tactic_option.cmt +lib/rocq-runtime/vernac/tactic_option.cmti +lib/rocq-runtime/vernac/tactic_option.cmx +lib/rocq-runtime/vernac/tactic_option.ml +lib/rocq-runtime/vernac/tactic_option.mli +lib/rocq-runtime/vernac/topfmt.cmi +lib/rocq-runtime/vernac/topfmt.cmt +lib/rocq-runtime/vernac/topfmt.cmti +lib/rocq-runtime/vernac/topfmt.cmx +lib/rocq-runtime/vernac/topfmt.ml +lib/rocq-runtime/vernac/topfmt.mli +lib/rocq-runtime/vernac/vernac.a +lib/rocq-runtime/vernac/vernac.cma +lib/rocq-runtime/vernac/vernac.cmxa +lib/rocq-runtime/vernac/vernac.cmxs +lib/rocq-runtime/vernac/vernacControl.cmi +lib/rocq-runtime/vernac/vernacControl.cmt +lib/rocq-runtime/vernac/vernacControl.cmti +lib/rocq-runtime/vernac/vernacControl.cmx +lib/rocq-runtime/vernac/vernacControl.ml +lib/rocq-runtime/vernac/vernacControl.mli +lib/rocq-runtime/vernac/vernac_classifier.cmi +lib/rocq-runtime/vernac/vernac_classifier.cmt +lib/rocq-runtime/vernac/vernac_classifier.cmti +lib/rocq-runtime/vernac/vernac_classifier.cmx +lib/rocq-runtime/vernac/vernac_classifier.ml +lib/rocq-runtime/vernac/vernac_classifier.mli +lib/rocq-runtime/vernac/vernacentries.cmi +lib/rocq-runtime/vernac/vernacentries.cmt +lib/rocq-runtime/vernac/vernacentries.cmti +lib/rocq-runtime/vernac/vernacentries.cmx +lib/rocq-runtime/vernac/vernacentries.ml +lib/rocq-runtime/vernac/vernacentries.mli +lib/rocq-runtime/vernac/vernacexpr.cmi +lib/rocq-runtime/vernac/vernacexpr.cmti +lib/rocq-runtime/vernac/vernacexpr.mli +lib/rocq-runtime/vernac/vernacextend.cmi +lib/rocq-runtime/vernac/vernacextend.cmt +lib/rocq-runtime/vernac/vernacextend.cmti +lib/rocq-runtime/vernac/vernacextend.cmx +lib/rocq-runtime/vernac/vernacextend.ml +lib/rocq-runtime/vernac/vernacextend.mli +lib/rocq-runtime/vernac/vernacinterp.cmi +lib/rocq-runtime/vernac/vernacinterp.cmt +lib/rocq-runtime/vernac/vernacinterp.cmti +lib/rocq-runtime/vernac/vernacinterp.cmx +lib/rocq-runtime/vernac/vernacinterp.ml +lib/rocq-runtime/vernac/vernacinterp.mli +lib/rocq-runtime/vernac/vernacoptions.cmi +lib/rocq-runtime/vernac/vernacoptions.cmt +lib/rocq-runtime/vernac/vernacoptions.cmti +lib/rocq-runtime/vernac/vernacoptions.cmx +lib/rocq-runtime/vernac/vernacoptions.ml +lib/rocq-runtime/vernac/vernacoptions.mli +lib/rocq-runtime/vernac/vernacprop.cmi +lib/rocq-runtime/vernac/vernacprop.cmt +lib/rocq-runtime/vernac/vernacprop.cmti +lib/rocq-runtime/vernac/vernacprop.cmx +lib/rocq-runtime/vernac/vernacprop.ml +lib/rocq-runtime/vernac/vernacprop.mli +lib/rocq-runtime/vernac/vernacstate.cmi +lib/rocq-runtime/vernac/vernacstate.cmt +lib/rocq-runtime/vernac/vernacstate.cmti +lib/rocq-runtime/vernac/vernacstate.cmx +lib/rocq-runtime/vernac/vernacstate.ml +lib/rocq-runtime/vernac/vernacstate.mli +lib/rocq-runtime/vernac/vernactypes.cmi +lib/rocq-runtime/vernac/vernactypes.cmt +lib/rocq-runtime/vernac/vernactypes.cmti +lib/rocq-runtime/vernac/vernactypes.cmx +lib/rocq-runtime/vernac/vernactypes.ml +lib/rocq-runtime/vernac/vernactypes.mli +lib/rocq-runtime/vm/coqrun.a +lib/rocq-runtime/vm/coqrun.cma +lib/rocq-runtime/vm/coqrun.cmi +lib/rocq-runtime/vm/coqrun.cmt +lib/rocq-runtime/vm/coqrun.cmx +lib/rocq-runtime/vm/coqrun.cmxa +lib/rocq-runtime/vm/coqrun.cmxs +lib/rocq-runtime/vm/coqrun.ml +lib/rocq-runtime/vm/libcoqrun_stubs.a +lib/rocq/dllcoqrun_stubs.so +%%IDE%%lib/rocqide/META +%%IDE%%lib/rocqide/dune-package +%%IDE%%lib/rocqide/opam +%%IDE%%share/coq/coq-ssreflect.lang +%%IDE%%share/coq/coq.lang +%%IDE%%share/coq/coq.png +%%IDE%%share/coq/coq_style.xml +%%IDE%%share/coq/default.bindings +share/doc/ocaml/coq-core/LICENSE +share/doc/ocaml/coq-core/README.md +%%IDE%%share/doc/ocaml/coqide-server/LICENSE +%%IDE%%share/doc/ocaml/coqide-server/README.md +share/doc/ocaml/rocq-core/LICENSE +share/doc/ocaml/rocq-core/README.md +share/doc/ocaml/rocq-runtime/LICENSE +share/doc/ocaml/rocq-runtime/README.md +%%IDE%%share/doc/ocaml/rocqide/LICENSE +%%IDE%%share/doc/ocaml/rocqide/README.md +%%IDE%%share/doc/ocaml/rocqide/odoc-pages/index.mld +share/man/man1/coq-tex.1.gz +share/man/man1/coq_makefile.1.gz +share/man/man1/coqc.1.gz +share/man/man1/coqchk.1.gz +share/man/man1/coqdep.1.gz +share/man/man1/coqdoc.1.gz +share/man/man1/coqnative.1.gz +share/man/man1/coqtop.1.gz +share/man/man1/coqtop.byte.1.gz +share/man/man1/coqwc.1.gz +share/man/man1/rocq.1.gz +share/man/man1/rocqchk.1.gz +%%IDE%%share/man/man1/rocqide.1.gz +%%TEXMFDIR%%/tex/latex/misc/coqdoc.sty +%%IDE%%@dir etc/xdg/coq +@dir %%OCAML_SITELIBDIR%% -- 2.53.0