Fedora Packages

coq-8.16.1-1.fc38 in Fedora Rawhide

↵ Return to the main page of coq
View build
Search for updates

Package Info (Data from x86_64 build)
🠗 Changelog
🠗 Dependencies
🠗 Provides
🠗 Files

Changelog

Date Author Change
2022-11-26 Jerry James <loganjerry at gmail dot com> - 8.16.1-1 - Version 8.16.1
2022-10-06 Jerry James <loganjerry at gmail dot com> - 8.16.0-2 - Remove the manual, which has a non-free license (bz 2132567)
2022-09-16 Jerry James <loganjerry at gmail dot com> - 8.16.0-1 - Version 8.16.0 - Drop upstreamed patch for Sphinx 4.5 support
2022-08-15 Jerry James <loganjerry at gmail dot com> - 8.15.2-3 - Convert License tags to SPDX
2022-07-20 Fedora Release Engineering <releng at fedoraproject dot org> - 8.15.2-3 - Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
2022-07-19 Karolina Surma <ksurma at redhat dot com> - 8.15.2-2 - Enable documentation build with Sphinx 5+
2022-07-19 Jerry James <loganjerry at gmail dot com> - 8.15.2-2 - Remove i686 support - Use new OCaml macros
2022-06-20 Jerry James <loganjerry at gmail dot com> - 8.15.2-2 - Rebuild for antlr4-project 4.10.1
2022-06-19 Richard W.M. Jones <rjones at redhat dot com> - 8.15.2-1 - Upgrade to 8.15.2 - OCaml 4.14.0 rebuild
2022-03-25 Jerry James <loganjerry at gmail dot com> - 8.15.1-1 - Version 8.15.1

Dependencies

Provides

  • coq
  • coq(x86-64)
  • ocaml(NCoq_Arith_Arith)
  • ocaml(NCoq_Arith_Arith_base)
  • ocaml(NCoq_Arith_Arith_prebase)
  • ocaml(NCoq_Arith_Between)
  • ocaml(NCoq_Arith_Bool_nat)
  • ocaml(NCoq_Arith_Cantor)
  • ocaml(NCoq_Arith_Compare)
  • ocaml(NCoq_Arith_Compare_dec)
  • ocaml(NCoq_Arith_Div2)
  • ocaml(NCoq_Arith_EqNat)
  • ocaml(NCoq_Arith_Euclid)
  • ocaml(NCoq_Arith_Even)
  • ocaml(NCoq_Arith_Factorial)
  • ocaml(NCoq_Arith_Gt)
  • ocaml(NCoq_Arith_Le)
  • ocaml(NCoq_Arith_Lt)
  • ocaml(NCoq_Arith_Max)
  • ocaml(NCoq_Arith_Min)
  • ocaml(NCoq_Arith_Minus)
  • ocaml(NCoq_Arith_Mult)
  • ocaml(NCoq_Arith_PeanoNat)
  • ocaml(NCoq_Arith_Peano_dec)
  • ocaml(NCoq_Arith_Plus)
  • ocaml(NCoq_Arith_Wf_nat)
  • ocaml(NCoq_Array_PArray)
  • ocaml(NCoq_Bool_Bool)
  • ocaml(NCoq_Bool_BoolEq)
  • ocaml(NCoq_Bool_BoolOrder)
  • ocaml(NCoq_Bool_Bvector)
  • ocaml(NCoq_Bool_DecBool)
  • ocaml(NCoq_Bool_IfProp)
  • ocaml(NCoq_Bool_Sumbool)
  • ocaml(NCoq_Bool_Zerob)
  • ocaml(NCoq_Classes_CEquivalence)
  • ocaml(NCoq_Classes_CMorphisms)
  • ocaml(NCoq_Classes_CRelationClasses)
  • ocaml(NCoq_Classes_DecidableClass)
  • ocaml(NCoq_Classes_EquivDec)
  • ocaml(NCoq_Classes_Equivalence)
  • ocaml(NCoq_Classes_Init)
  • ocaml(NCoq_Classes_Morphisms)
  • ocaml(NCoq_Classes_Morphisms_Prop)
  • ocaml(NCoq_Classes_Morphisms_Relations)
  • ocaml(NCoq_Classes_RelationClasses)
  • ocaml(NCoq_Classes_RelationPairs)
  • ocaml(NCoq_Classes_SetoidClass)
  • ocaml(NCoq_Classes_SetoidDec)
  • ocaml(NCoq_Classes_SetoidTactics)
  • ocaml(NCoq_Compat_AdmitAxiom)
  • ocaml(NCoq_Compat_Coq814)
  • ocaml(NCoq_Compat_Coq815)
  • ocaml(NCoq_Compat_Coq816)
  • ocaml(NCoq_FSets_FMapAVL)
  • ocaml(NCoq_FSets_FMapFacts)
  • ocaml(NCoq_FSets_FMapFullAVL)
  • ocaml(NCoq_FSets_FMapInterface)
  • ocaml(NCoq_FSets_FMapList)
  • ocaml(NCoq_FSets_FMapPositive)
  • ocaml(NCoq_FSets_FMapWeakList)
  • ocaml(NCoq_FSets_FMaps)
  • ocaml(NCoq_FSets_FSetAVL)
  • ocaml(NCoq_FSets_FSetBridge)
  • ocaml(NCoq_FSets_FSetCompat)
  • ocaml(NCoq_FSets_FSetDecide)
  • ocaml(NCoq_FSets_FSetEqProperties)
  • ocaml(NCoq_FSets_FSetFacts)
  • ocaml(NCoq_FSets_FSetInterface)
  • ocaml(NCoq_FSets_FSetList)
  • ocaml(NCoq_FSets_FSetPositive)
  • ocaml(NCoq_FSets_FSetProperties)
  • ocaml(NCoq_FSets_FSetToFiniteSet)
  • ocaml(NCoq_FSets_FSetWeakList)
  • ocaml(NCoq_FSets_FSets)
  • ocaml(NCoq_Floats_FloatAxioms)
  • ocaml(NCoq_Floats_FloatClass)
  • ocaml(NCoq_Floats_FloatLemmas)
  • ocaml(NCoq_Floats_FloatOps)
  • ocaml(NCoq_Floats_Floats)
  • ocaml(NCoq_Floats_PrimFloat)
  • ocaml(NCoq_Floats_SpecFloat)
  • ocaml(NCoq_Init_Byte)
  • ocaml(NCoq_Init_Datatypes)
  • ocaml(NCoq_Init_Decimal)
  • ocaml(NCoq_Init_Hexadecimal)
  • ocaml(NCoq_Init_Logic)
  • ocaml(NCoq_Init_Ltac)
  • ocaml(NCoq_Init_Nat)
  • ocaml(NCoq_Init_Notations)
  • ocaml(NCoq_Init_Number)
  • ocaml(NCoq_Init_Peano)
  • ocaml(NCoq_Init_Prelude)
  • ocaml(NCoq_Init_Specif)
  • ocaml(NCoq_Init_Tactics)
  • ocaml(NCoq_Init_Tauto)
  • ocaml(NCoq_Init_Wf)
  • ocaml(NCoq_Lists_List)
  • ocaml(NCoq_Lists_ListDec)
  • ocaml(NCoq_Lists_ListSet)
  • ocaml(NCoq_Lists_ListTactics)
  • ocaml(NCoq_Lists_SetoidList)
  • ocaml(NCoq_Lists_SetoidPermutation)
  • ocaml(NCoq_Lists_StreamMemo)
  • ocaml(NCoq_Lists_Streams)
  • ocaml(NCoq_Logic_Adjointification)
  • ocaml(NCoq_Logic_Berardi)
  • ocaml(NCoq_Logic_ChoiceFacts)
  • ocaml(NCoq_Logic_Classical)
  • ocaml(NCoq_Logic_ClassicalChoice)
  • ocaml(NCoq_Logic_ClassicalDescription)
  • ocaml(NCoq_Logic_ClassicalEpsilon)
  • ocaml(NCoq_Logic_ClassicalFacts)
  • ocaml(NCoq_Logic_ClassicalUniqueChoice)
  • ocaml(NCoq_Logic_Classical_Pred_Type)
  • ocaml(NCoq_Logic_Classical_Prop)
  • ocaml(NCoq_Logic_ConstructiveEpsilon)
  • ocaml(NCoq_Logic_Decidable)
  • ocaml(NCoq_Logic_Description)
  • ocaml(NCoq_Logic_Diaconescu)
  • ocaml(NCoq_Logic_Epsilon)
  • ocaml(NCoq_Logic_Eqdep)
  • ocaml(NCoq_Logic_EqdepFacts)
  • ocaml(NCoq_Logic_Eqdep_dec)
  • ocaml(NCoq_Logic_ExtensionalFunctionRepresentative)
  • ocaml(NCoq_Logic_ExtensionalityFacts)
  • ocaml(NCoq_Logic_FinFun)
  • ocaml(NCoq_Logic_FunctionalExtensionality)
  • ocaml(NCoq_Logic_HLevels)
  • ocaml(NCoq_Logic_Hurkens)
  • ocaml(NCoq_Logic_IndefiniteDescription)
  • ocaml(NCoq_Logic_JMeq)
  • ocaml(NCoq_Logic_ProofIrrelevance)
  • ocaml(NCoq_Logic_ProofIrrelevanceFacts)
  • ocaml(NCoq_Logic_PropExtensionality)
  • ocaml(NCoq_Logic_PropExtensionalityFacts)
  • ocaml(NCoq_Logic_PropFacts)
  • ocaml(NCoq_Logic_RelationalChoice)
  • ocaml(NCoq_Logic_SetIsType)
  • ocaml(NCoq_Logic_SetoidChoice)
  • ocaml(NCoq_Logic_StrictProp)
  • ocaml(NCoq_Logic_WKL)
  • ocaml(NCoq_Logic_WeakFan)
  • ocaml(NCoq_MSets_MSetAVL)
  • ocaml(NCoq_MSets_MSetDecide)
  • ocaml(NCoq_MSets_MSetEqProperties)
  • ocaml(NCoq_MSets_MSetFacts)
  • ocaml(NCoq_MSets_MSetGenTree)
  • ocaml(NCoq_MSets_MSetInterface)
  • ocaml(NCoq_MSets_MSetList)
  • ocaml(NCoq_MSets_MSetPositive)
  • ocaml(NCoq_MSets_MSetProperties)
  • ocaml(NCoq_MSets_MSetRBT)
  • ocaml(NCoq_MSets_MSetToFiniteSet)
  • ocaml(NCoq_MSets_MSetWeakList)
  • ocaml(NCoq_MSets_MSets)
  • ocaml(NCoq_NArith_BinNat)
  • ocaml(NCoq_NArith_BinNatDef)
  • ocaml(NCoq_NArith_NArith)
  • ocaml(NCoq_NArith_Ndec)
  • ocaml(NCoq_NArith_Ndigits)
  • ocaml(NCoq_NArith_Ndist)
  • ocaml(NCoq_NArith_Ndiv_def)
  • ocaml(NCoq_NArith_Ngcd_def)
  • ocaml(NCoq_NArith_Nnat)
  • ocaml(NCoq_NArith_Nsqrt_def)
  • ocaml(NCoq_Numbers_AltBinNotations)
  • ocaml(NCoq_Numbers_BinNums)
  • ocaml(NCoq_Numbers_Cyclic_Abstract_CarryType)
  • ocaml(NCoq_Numbers_Cyclic_Abstract_CyclicAxioms)
  • ocaml(NCoq_Numbers_Cyclic_Abstract_DoubleType)
  • ocaml(NCoq_Numbers_Cyclic_Abstract_NZCyclic)
  • ocaml(NCoq_Numbers_Cyclic_Int31_Cyclic31)
  • ocaml(NCoq_Numbers_Cyclic_Int31_Int31)
  • ocaml(NCoq_Numbers_Cyclic_Int31_Ring31)
  • ocaml(NCoq_Numbers_Cyclic_Int63_Cyclic63)
  • ocaml(NCoq_Numbers_Cyclic_Int63_PrimInt63)
  • ocaml(NCoq_Numbers_Cyclic_Int63_Ring63)
  • ocaml(NCoq_Numbers_Cyclic_Int63_Sint63)
  • ocaml(NCoq_Numbers_Cyclic_Int63_Uint63)
  • ocaml(NCoq_Numbers_Cyclic_ZModulo_ZModulo)
  • ocaml(NCoq_Numbers_DecimalFacts)
  • ocaml(NCoq_Numbers_DecimalN)
  • ocaml(NCoq_Numbers_DecimalNat)
  • ocaml(NCoq_Numbers_DecimalPos)
  • ocaml(NCoq_Numbers_DecimalQ)
  • ocaml(NCoq_Numbers_DecimalR)
  • ocaml(NCoq_Numbers_DecimalString)
  • ocaml(NCoq_Numbers_DecimalZ)
  • ocaml(NCoq_Numbers_HexadecimalFacts)
  • ocaml(NCoq_Numbers_HexadecimalN)
  • ocaml(NCoq_Numbers_HexadecimalNat)
  • ocaml(NCoq_Numbers_HexadecimalPos)
  • ocaml(NCoq_Numbers_HexadecimalQ)
  • ocaml(NCoq_Numbers_HexadecimalR)
  • ocaml(NCoq_Numbers_HexadecimalString)
  • ocaml(NCoq_Numbers_HexadecimalZ)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZAdd)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZAddOrder)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZAxioms)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZBase)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZBits)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZDivEucl)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZDivFloor)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZDivTrunc)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZGcd)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZLcm)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZLt)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZMaxMin)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZMul)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZMulOrder)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZParity)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZPow)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZProperties)
  • ocaml(NCoq_Numbers_Integer_Abstract_ZSgnAbs)
  • ocaml(NCoq_Numbers_Integer_Binary_ZBinary)
  • ocaml(NCoq_Numbers_Integer_NatPairs_ZNatPairs)
  • ocaml(NCoq_Numbers_NaryFunctions)
  • ocaml(NCoq_Numbers_NatInt_NZAdd)
  • ocaml(NCoq_Numbers_NatInt_NZAddOrder)
  • ocaml(NCoq_Numbers_NatInt_NZAxioms)
  • ocaml(NCoq_Numbers_NatInt_NZBase)
  • ocaml(NCoq_Numbers_NatInt_NZBits)
  • ocaml(NCoq_Numbers_NatInt_NZDiv)
  • ocaml(NCoq_Numbers_NatInt_NZDomain)
  • ocaml(NCoq_Numbers_NatInt_NZGcd)
  • ocaml(NCoq_Numbers_NatInt_NZLog)
  • ocaml(NCoq_Numbers_NatInt_NZMul)
  • ocaml(NCoq_Numbers_NatInt_NZMulOrder)
  • ocaml(NCoq_Numbers_NatInt_NZOrder)
  • ocaml(NCoq_Numbers_NatInt_NZParity)
  • ocaml(NCoq_Numbers_NatInt_NZPow)
  • ocaml(NCoq_Numbers_NatInt_NZProperties)
  • ocaml(NCoq_Numbers_NatInt_NZSqrt)
  • ocaml(NCoq_Numbers_Natural_Abstract_NAdd)
  • ocaml(NCoq_Numbers_Natural_Abstract_NAddOrder)
  • ocaml(NCoq_Numbers_Natural_Abstract_NAxioms)
  • ocaml(NCoq_Numbers_Natural_Abstract_NBase)
  • ocaml(NCoq_Numbers_Natural_Abstract_NBits)
  • ocaml(NCoq_Numbers_Natural_Abstract_NDefOps)
  • ocaml(NCoq_Numbers_Natural_Abstract_NDiv)
  • ocaml(NCoq_Numbers_Natural_Abstract_NGcd)
  • ocaml(NCoq_Numbers_Natural_Abstract_NIso)
  • ocaml(NCoq_Numbers_Natural_Abstract_NLcm)
  • ocaml(NCoq_Numbers_Natural_Abstract_NLog)
  • ocaml(NCoq_Numbers_Natural_Abstract_NMaxMin)
  • ocaml(NCoq_Numbers_Natural_Abstract_NMulOrder)
  • ocaml(NCoq_Numbers_Natural_Abstract_NOrder)
  • ocaml(NCoq_Numbers_Natural_Abstract_NParity)
  • ocaml(NCoq_Numbers_Natural_Abstract_NPow)
  • ocaml(NCoq_Numbers_Natural_Abstract_NProperties)
  • ocaml(NCoq_Numbers_Natural_Abstract_NSqrt)
  • ocaml(NCoq_Numbers_Natural_Abstract_NStrongRec)
  • ocaml(NCoq_Numbers_Natural_Abstract_NSub)
  • ocaml(NCoq_Numbers_Natural_Binary_NBinary)
  • ocaml(NCoq_Numbers_Natural_Peano_NPeano)
  • ocaml(NCoq_Numbers_NumPrelude)
  • ocaml(NCoq_PArith_BinPos)
  • ocaml(NCoq_PArith_BinPosDef)
  • ocaml(NCoq_PArith_PArith)
  • ocaml(NCoq_PArith_POrderedType)
  • ocaml(NCoq_PArith_Pnat)
  • ocaml(NCoq_Program_Basics)
  • ocaml(NCoq_Program_Combinators)
  • ocaml(NCoq_Program_Equality)
  • ocaml(NCoq_Program_Program)
  • ocaml(NCoq_Program_Subset)
  • ocaml(NCoq_Program_Syntax)
  • ocaml(NCoq_Program_Tactics)
  • ocaml(NCoq_Program_Utils)
  • ocaml(NCoq_Program_Wf)
  • ocaml(NCoq_QArith_QArith)
  • ocaml(NCoq_QArith_QArith_base)
  • ocaml(NCoq_QArith_QOrderedType)
  • ocaml(NCoq_QArith_Qabs)
  • ocaml(NCoq_QArith_Qcabs)
  • ocaml(NCoq_QArith_Qcanon)
  • ocaml(NCoq_QArith_Qfield)
  • ocaml(NCoq_QArith_Qminmax)
  • ocaml(NCoq_QArith_Qpower)
  • ocaml(NCoq_QArith_Qreals)
  • ocaml(NCoq_QArith_Qreduction)
  • ocaml(NCoq_QArith_Qring)
  • ocaml(NCoq_QArith_Qround)
  • ocaml(NCoq_Reals_Abstract_ConstructiveAbs)
  • ocaml(NCoq_Reals_Abstract_ConstructiveLUB)
  • ocaml(NCoq_Reals_Abstract_ConstructiveLimits)
  • ocaml(NCoq_Reals_Abstract_ConstructiveMinMax)
  • ocaml(NCoq_Reals_Abstract_ConstructivePower)
  • ocaml(NCoq_Reals_Abstract_ConstructiveReals)
  • ocaml(NCoq_Reals_Abstract_ConstructiveRealsMorphisms)
  • ocaml(NCoq_Reals_Abstract_ConstructiveSum)
  • ocaml(NCoq_Reals_Alembert)
  • ocaml(NCoq_Reals_AltSeries)
  • ocaml(NCoq_Reals_ArithProp)
  • ocaml(NCoq_Reals_Binomial)
  • ocaml(NCoq_Reals_Cauchy_ConstructiveCauchyAbs)
  • ocaml(NCoq_Reals_Cauchy_ConstructiveCauchyReals)
  • ocaml(NCoq_Reals_Cauchy_ConstructiveCauchyRealsMult)
  • ocaml(NCoq_Reals_Cauchy_ConstructiveExtra)
  • ocaml(NCoq_Reals_Cauchy_ConstructiveRcomplete)
  • ocaml(NCoq_Reals_Cauchy_PosExtra)
  • ocaml(NCoq_Reals_Cauchy_QExtra)
  • ocaml(NCoq_Reals_Cauchy_prod)
  • ocaml(NCoq_Reals_ClassicalConstructiveReals)
  • ocaml(NCoq_Reals_ClassicalDedekindReals)
  • ocaml(NCoq_Reals_Cos_plus)
  • ocaml(NCoq_Reals_Cos_rel)
  • ocaml(NCoq_Reals_DiscrR)
  • ocaml(NCoq_Reals_Exp_prop)
  • ocaml(NCoq_Reals_Integration)
  • ocaml(NCoq_Reals_MVT)
  • ocaml(NCoq_Reals_Machin)
  • ocaml(NCoq_Reals_NewtonInt)
  • ocaml(NCoq_Reals_PSeries_reg)
  • ocaml(NCoq_Reals_PartSum)
  • ocaml(NCoq_Reals_RIneq)
  • ocaml(NCoq_Reals_RList)
  • ocaml(NCoq_Reals_ROrderedType)
  • ocaml(NCoq_Reals_R_Ifp)
  • ocaml(NCoq_Reals_R_sqr)
  • ocaml(NCoq_Reals_R_sqrt)
  • ocaml(NCoq_Reals_Ranalysis)
  • ocaml(NCoq_Reals_Ranalysis1)
  • ocaml(NCoq_Reals_Ranalysis2)
  • ocaml(NCoq_Reals_Ranalysis3)
  • ocaml(NCoq_Reals_Ranalysis4)
  • ocaml(NCoq_Reals_Ranalysis5)
  • ocaml(NCoq_Reals_Ranalysis_reg)
  • ocaml(NCoq_Reals_Ratan)
  • ocaml(NCoq_Reals_Raxioms)
  • ocaml(NCoq_Reals_Rbase)
  • ocaml(NCoq_Reals_Rbasic_fun)
  • ocaml(NCoq_Reals_Rcomplete)
  • ocaml(NCoq_Reals_Rdefinitions)
  • ocaml(NCoq_Reals_Rderiv)
  • ocaml(NCoq_Reals_Reals)
  • ocaml(NCoq_Reals_Rfunctions)
  • ocaml(NCoq_Reals_Rgeom)
  • ocaml(NCoq_Reals_RiemannInt)
  • ocaml(NCoq_Reals_RiemannInt_SF)
  • ocaml(NCoq_Reals_Rlimit)
  • ocaml(NCoq_Reals_Rlogic)
  • ocaml(NCoq_Reals_Rminmax)
  • ocaml(NCoq_Reals_Rpow_def)
  • ocaml(NCoq_Reals_Rpower)
  • ocaml(NCoq_Reals_Rprod)
  • ocaml(NCoq_Reals_Rregisternames)
  • ocaml(NCoq_Reals_Rseries)
  • ocaml(NCoq_Reals_Rsigma)
  • ocaml(NCoq_Reals_Rsqrt_def)
  • ocaml(NCoq_Reals_Rtopology)
  • ocaml(NCoq_Reals_Rtrigo)
  • ocaml(NCoq_Reals_Rtrigo1)
  • ocaml(NCoq_Reals_Rtrigo_alt)
  • ocaml(NCoq_Reals_Rtrigo_calc)
  • ocaml(NCoq_Reals_Rtrigo_def)
  • ocaml(NCoq_Reals_Rtrigo_facts)
  • ocaml(NCoq_Reals_Rtrigo_fun)
  • ocaml(NCoq_Reals_Rtrigo_reg)
  • ocaml(NCoq_Reals_Runcountable)
  • ocaml(NCoq_Reals_SeqProp)
  • ocaml(NCoq_Reals_SeqSeries)
  • ocaml(NCoq_Reals_SplitAbsolu)
  • ocaml(NCoq_Reals_SplitRmult)
  • ocaml(NCoq_Reals_Sqrt_reg)
  • ocaml(NCoq_Relations_Operators_Properties)
  • ocaml(NCoq_Relations_Relation_Definitions)
  • ocaml(NCoq_Relations_Relation_Operators)
  • ocaml(NCoq_Relations_Relations)
  • ocaml(NCoq_Setoids_Setoid)
  • ocaml(NCoq_Sets_Classical_sets)
  • ocaml(NCoq_Sets_Constructive_sets)
  • ocaml(NCoq_Sets_Cpo)
  • ocaml(NCoq_Sets_Ensembles)
  • ocaml(NCoq_Sets_Finite_sets)
  • ocaml(NCoq_Sets_Finite_sets_facts)
  • ocaml(NCoq_Sets_Image)
  • ocaml(NCoq_Sets_Infinite_sets)
  • ocaml(NCoq_Sets_Integers)
  • ocaml(NCoq_Sets_Multiset)
  • ocaml(NCoq_Sets_Partial_Order)
  • ocaml(NCoq_Sets_Permut)
  • ocaml(NCoq_Sets_Powerset)
  • ocaml(NCoq_Sets_Powerset_Classical_facts)
  • ocaml(NCoq_Sets_Powerset_facts)
  • ocaml(NCoq_Sets_Relations_1)
  • ocaml(NCoq_Sets_Relations_1_facts)
  • ocaml(NCoq_Sets_Relations_2)
  • ocaml(NCoq_Sets_Relations_2_facts)
  • ocaml(NCoq_Sets_Relations_3)
  • ocaml(NCoq_Sets_Relations_3_facts)
  • ocaml(NCoq_Sets_Uniset)
  • ocaml(NCoq_Sorting_CPermutation)
  • ocaml(NCoq_Sorting_Heap)
  • ocaml(NCoq_Sorting_Mergesort)
  • ocaml(NCoq_Sorting_PermutEq)
  • ocaml(NCoq_Sorting_PermutSetoid)
  • ocaml(NCoq_Sorting_Permutation)
  • ocaml(NCoq_Sorting_Sorted)
  • ocaml(NCoq_Sorting_Sorting)
  • ocaml(NCoq_Strings_Ascii)
  • ocaml(NCoq_Strings_BinaryString)
  • ocaml(NCoq_Strings_Byte)
  • ocaml(NCoq_Strings_ByteVector)
  • ocaml(NCoq_Strings_HexString)
  • ocaml(NCoq_Strings_OctalString)
  • ocaml(NCoq_Strings_String)
  • ocaml(NCoq_Structures_DecidableType)
  • ocaml(NCoq_Structures_DecidableTypeEx)
  • ocaml(NCoq_Structures_Equalities)
  • ocaml(NCoq_Structures_EqualitiesFacts)
  • ocaml(NCoq_Structures_GenericMinMax)
  • ocaml(NCoq_Structures_OrderedType)
  • ocaml(NCoq_Structures_OrderedTypeAlt)
  • ocaml(NCoq_Structures_OrderedTypeEx)
  • ocaml(NCoq_Structures_Orders)
  • ocaml(NCoq_Structures_OrdersAlt)
  • ocaml(NCoq_Structures_OrdersEx)
  • ocaml(NCoq_Structures_OrdersFacts)
  • ocaml(NCoq_Structures_OrdersLists)
  • ocaml(NCoq_Structures_OrdersTac)
  • ocaml(NCoq_Unicode_Utf8)
  • ocaml(NCoq_Unicode_Utf8_core)
  • ocaml(NCoq_Vectors_Fin)
  • ocaml(NCoq_Vectors_Vector)
  • ocaml(NCoq_Vectors_VectorDef)
  • ocaml(NCoq_Vectors_VectorEq)
  • ocaml(NCoq_Vectors_VectorSpec)
  • ocaml(NCoq_Wellfounded_Disjoint_Union)
  • ocaml(NCoq_Wellfounded_Inclusion)
  • ocaml(NCoq_Wellfounded_Inverse_Image)
  • ocaml(NCoq_Wellfounded_Lexicographic_Exponentiation)
  • ocaml(NCoq_Wellfounded_Lexicographic_Product)
  • ocaml(NCoq_Wellfounded_Transitive_Closure)
  • ocaml(NCoq_Wellfounded_Union)
  • ocaml(NCoq_Wellfounded_Well_Ordering)
  • ocaml(NCoq_Wellfounded_Wellfounded)
  • ocaml(NCoq_ZArith_BinInt)
  • ocaml(NCoq_ZArith_BinIntDef)
  • ocaml(NCoq_ZArith_Int)
  • ocaml(NCoq_ZArith_Wf_Z)
  • ocaml(NCoq_ZArith_ZArith)
  • ocaml(NCoq_ZArith_ZArith_base)
  • ocaml(NCoq_ZArith_ZArith_dec)
  • ocaml(NCoq_ZArith_Zabs)
  • ocaml(NCoq_ZArith_Zbool)
  • ocaml(NCoq_ZArith_Zcompare)
  • ocaml(NCoq_ZArith_Zcomplements)
  • ocaml(NCoq_ZArith_Zdigits)
  • ocaml(NCoq_ZArith_Zdiv)
  • ocaml(NCoq_ZArith_Zeuclid)
  • ocaml(NCoq_ZArith_Zeven)
  • ocaml(NCoq_ZArith_Zgcd_alt)
  • ocaml(NCoq_ZArith_Zhints)
  • ocaml(NCoq_ZArith_Zmax)
  • ocaml(NCoq_ZArith_Zmin)
  • ocaml(NCoq_ZArith_Zminmax)
  • ocaml(NCoq_ZArith_Zmisc)
  • ocaml(NCoq_ZArith_Znat)
  • ocaml(NCoq_ZArith_Znumtheory)
  • ocaml(NCoq_ZArith_Zorder)
  • ocaml(NCoq_ZArith_Zpow_alt)
  • ocaml(NCoq_ZArith_Zpow_def)
  • ocaml(NCoq_ZArith_Zpow_facts)
  • ocaml(NCoq_ZArith_Zpower)
  • ocaml(NCoq_ZArith_Zquot)
  • ocaml(NCoq_ZArith_Zwf)
  • ocaml(NCoq_ZArith_auxiliary)
  • ocaml(NCoq_btauto_Algebra)
  • ocaml(NCoq_btauto_Btauto)
  • ocaml(NCoq_btauto_Reflect)
  • ocaml(NCoq_derive_Derive)
  • ocaml(NCoq_extraction_ExtrHaskellBasic)
  • ocaml(NCoq_extraction_ExtrHaskellNatInt)
  • ocaml(NCoq_extraction_ExtrHaskellNatInteger)
  • ocaml(NCoq_extraction_ExtrHaskellNatNum)
  • ocaml(NCoq_extraction_ExtrHaskellString)
  • ocaml(NCoq_extraction_ExtrHaskellZInt)
  • ocaml(NCoq_extraction_ExtrHaskellZInteger)
  • ocaml(NCoq_extraction_ExtrHaskellZNum)
  • ocaml(NCoq_extraction_ExtrOCamlFloats)
  • ocaml(NCoq_extraction_ExtrOCamlInt63)
  • ocaml(NCoq_extraction_ExtrOCamlPArray)
  • ocaml(NCoq_extraction_ExtrOcamlBasic)
  • ocaml(NCoq_extraction_ExtrOcamlChar)
  • ocaml(NCoq_extraction_ExtrOcamlIntConv)
  • ocaml(NCoq_extraction_ExtrOcamlNatBigInt)
  • ocaml(NCoq_extraction_ExtrOcamlNatInt)
  • ocaml(NCoq_extraction_ExtrOcamlNativeString)
  • ocaml(NCoq_extraction_ExtrOcamlString)
  • ocaml(NCoq_extraction_ExtrOcamlZBigInt)
  • ocaml(NCoq_extraction_ExtrOcamlZInt)
  • ocaml(NCoq_extraction_Extraction)
  • ocaml(NCoq_funind_FunInd)
  • ocaml(NCoq_funind_Recdef)
  • ocaml(NCoq_micromega_DeclConstant)
  • ocaml(NCoq_micromega_Env)
  • ocaml(NCoq_micromega_EnvRing)
  • ocaml(NCoq_micromega_Fourier)
  • ocaml(NCoq_micromega_Fourier_util)
  • ocaml(NCoq_micromega_Lia)
  • ocaml(NCoq_micromega_Lqa)
  • ocaml(NCoq_micromega_Lra)
  • ocaml(NCoq_micromega_MExtraction)
  • ocaml(NCoq_micromega_OrderedRing)
  • ocaml(NCoq_micromega_Psatz)
  • ocaml(NCoq_micromega_QMicromega)
  • ocaml(NCoq_micromega_RMicromega)
  • ocaml(NCoq_micromega_Refl)
  • ocaml(NCoq_micromega_RingMicromega)
  • ocaml(NCoq_micromega_Tauto)
  • ocaml(NCoq_micromega_VarMap)
  • ocaml(NCoq_micromega_ZArith_hints)
  • ocaml(NCoq_micromega_ZCoeff)
  • ocaml(NCoq_micromega_ZMicromega)
  • ocaml(NCoq_micromega_Zify)
  • ocaml(NCoq_micromega_ZifyBool)
  • ocaml(NCoq_micromega_ZifyClasses)
  • ocaml(NCoq_micromega_ZifyComparison)
  • ocaml(NCoq_micromega_ZifyInst)
  • ocaml(NCoq_micromega_ZifyN)
  • ocaml(NCoq_micromega_ZifyNat)
  • ocaml(NCoq_micromega_ZifyPow)
  • ocaml(NCoq_micromega_ZifySint63)
  • ocaml(NCoq_micromega_ZifyUint63)
  • ocaml(NCoq_micromega_Ztac)
  • ocaml(NCoq_nsatz_Nsatz)
  • ocaml(NCoq_nsatz_NsatzTactic)
  • ocaml(NCoq_omega_OmegaLemmas)
  • ocaml(NCoq_omega_PreOmega)
  • ocaml(NCoq_rtauto_Bintree)
  • ocaml(NCoq_rtauto_Rtauto)
  • ocaml(NCoq_setoid_ring_Algebra_syntax)
  • ocaml(NCoq_setoid_ring_ArithRing)
  • ocaml(NCoq_setoid_ring_BinList)
  • ocaml(NCoq_setoid_ring_Cring)
  • ocaml(NCoq_setoid_ring_Field)
  • ocaml(NCoq_setoid_ring_Field_tac)
  • ocaml(NCoq_setoid_ring_Field_theory)
  • ocaml(NCoq_setoid_ring_InitialRing)
  • ocaml(NCoq_setoid_ring_Integral_domain)
  • ocaml(NCoq_setoid_ring_NArithRing)
  • ocaml(NCoq_setoid_ring_Ncring)
  • ocaml(NCoq_setoid_ring_Ncring_initial)
  • ocaml(NCoq_setoid_ring_Ncring_polynom)
  • ocaml(NCoq_setoid_ring_Ncring_tac)
  • ocaml(NCoq_setoid_ring_RealField)
  • ocaml(NCoq_setoid_ring_Ring)
  • ocaml(NCoq_setoid_ring_Ring_base)
  • ocaml(NCoq_setoid_ring_Ring_polynom)
  • ocaml(NCoq_setoid_ring_Ring_tac)
  • ocaml(NCoq_setoid_ring_Ring_theory)
  • ocaml(NCoq_setoid_ring_Rings_Q)
  • ocaml(NCoq_setoid_ring_Rings_R)
  • ocaml(NCoq_setoid_ring_Rings_Z)
  • ocaml(NCoq_setoid_ring_ZArithRing)
  • ocaml(NCoq_ssr_ssrbool)
  • ocaml(NCoq_ssr_ssrclasses)
  • ocaml(NCoq_ssr_ssreflect)
  • ocaml(NCoq_ssr_ssrfun)
  • ocaml(NCoq_ssr_ssrsetoid)
  • ocaml(NCoq_ssr_ssrunder)
  • ocaml(NCoq_ssrmatching_ssrmatching)
  • ocaml(NLtac2_Array)
  • ocaml(NLtac2_Bool)
  • ocaml(NLtac2_Char)
  • ocaml(NLtac2_Constr)
  • ocaml(NLtac2_Control)
  • ocaml(NLtac2_Env)
  • ocaml(NLtac2_Fresh)
  • ocaml(NLtac2_Ident)
  • ocaml(NLtac2_Ind)
  • ocaml(NLtac2_Init)
  • ocaml(NLtac2_Int)
  • ocaml(NLtac2_List)
  • ocaml(NLtac2_Ltac1)
  • ocaml(NLtac2_Ltac2)
  • ocaml(NLtac2_Message)
  • ocaml(NLtac2_Notations)
  • ocaml(NLtac2_Option)
  • ocaml(NLtac2_Pattern)
  • ocaml(NLtac2_Printf)
  • ocaml(NLtac2_Std)
  • ocaml(NLtac2_String)
  • ocamlx(NCoq_Arith_Arith)
  • ocamlx(NCoq_Arith_Arith_base)
  • ocamlx(NCoq_Arith_Arith_prebase)
  • ocamlx(NCoq_Arith_Between)
  • ocamlx(NCoq_Arith_Bool_nat)
  • ocamlx(NCoq_Arith_Cantor)
  • ocamlx(NCoq_Arith_Compare)
  • ocamlx(NCoq_Arith_Compare_dec)
  • ocamlx(NCoq_Arith_Div2)
  • ocamlx(NCoq_Arith_EqNat)
  • ocamlx(NCoq_Arith_Euclid)
  • ocamlx(NCoq_Arith_Even)
  • ocamlx(NCoq_Arith_Factorial)
  • ocamlx(NCoq_Arith_Gt)
  • ocamlx(NCoq_Arith_Le)
  • ocamlx(NCoq_Arith_Lt)
  • ocamlx(NCoq_Arith_Max)
  • ocamlx(NCoq_Arith_Min)
  • ocamlx(NCoq_Arith_Minus)
  • ocamlx(NCoq_Arith_Mult)
  • ocamlx(NCoq_Arith_PeanoNat)
  • ocamlx(NCoq_Arith_Peano_dec)
  • ocamlx(NCoq_Arith_Plus)
  • ocamlx(NCoq_Arith_Wf_nat)
  • ocamlx(NCoq_Array_PArray)
  • ocamlx(NCoq_Bool_Bool)
  • ocamlx(NCoq_Bool_BoolEq)
  • ocamlx(NCoq_Bool_BoolOrder)
  • ocamlx(NCoq_Bool_Bvector)
  • ocamlx(NCoq_Bool_DecBool)
  • ocamlx(NCoq_Bool_IfProp)
  • ocamlx(NCoq_Bool_Sumbool)
  • ocamlx(NCoq_Bool_Zerob)
  • ocamlx(NCoq_Classes_CEquivalence)
  • ocamlx(NCoq_Classes_CMorphisms)
  • ocamlx(NCoq_Classes_CRelationClasses)
  • ocamlx(NCoq_Classes_DecidableClass)
  • ocamlx(NCoq_Classes_EquivDec)
  • ocamlx(NCoq_Classes_Equivalence)
  • ocamlx(NCoq_Classes_Init)
  • ocamlx(NCoq_Classes_Morphisms)
  • ocamlx(NCoq_Classes_Morphisms_Prop)
  • ocamlx(NCoq_Classes_Morphisms_Relations)
  • ocamlx(NCoq_Classes_RelationClasses)
  • ocamlx(NCoq_Classes_RelationPairs)
  • ocamlx(NCoq_Classes_SetoidClass)
  • ocamlx(NCoq_Classes_SetoidDec)
  • ocamlx(NCoq_Classes_SetoidTactics)
  • ocamlx(NCoq_Compat_AdmitAxiom)
  • ocamlx(NCoq_Compat_Coq814)
  • ocamlx(NCoq_Compat_Coq815)
  • ocamlx(NCoq_Compat_Coq816)
  • ocamlx(NCoq_FSets_FMapAVL)
  • ocamlx(NCoq_FSets_FMapFacts)
  • ocamlx(NCoq_FSets_FMapFullAVL)
  • ocamlx(NCoq_FSets_FMapInterface)
  • ocamlx(NCoq_FSets_FMapList)
  • ocamlx(NCoq_FSets_FMapPositive)
  • ocamlx(NCoq_FSets_FMapWeakList)
  • ocamlx(NCoq_FSets_FMaps)
  • ocamlx(NCoq_FSets_FSetAVL)
  • ocamlx(NCoq_FSets_FSetBridge)
  • ocamlx(NCoq_FSets_FSetCompat)
  • ocamlx(NCoq_FSets_FSetDecide)
  • ocamlx(NCoq_FSets_FSetEqProperties)
  • ocamlx(NCoq_FSets_FSetFacts)
  • ocamlx(NCoq_FSets_FSetInterface)
  • ocamlx(NCoq_FSets_FSetList)
  • ocamlx(NCoq_FSets_FSetPositive)
  • ocamlx(NCoq_FSets_FSetProperties)
  • ocamlx(NCoq_FSets_FSetToFiniteSet)
  • ocamlx(NCoq_FSets_FSetWeakList)
  • ocamlx(NCoq_FSets_FSets)
  • ocamlx(NCoq_Floats_FloatAxioms)
  • ocamlx(NCoq_Floats_FloatClass)
  • ocamlx(NCoq_Floats_FloatLemmas)
  • ocamlx(NCoq_Floats_FloatOps)
  • ocamlx(NCoq_Floats_Floats)
  • ocamlx(NCoq_Floats_PrimFloat)
  • ocamlx(NCoq_Floats_SpecFloat)
  • ocamlx(NCoq_Init_Byte)
  • ocamlx(NCoq_Init_Datatypes)
  • ocamlx(NCoq_Init_Decimal)
  • ocamlx(NCoq_Init_Hexadecimal)
  • ocamlx(NCoq_Init_Logic)
  • ocamlx(NCoq_Init_Ltac)
  • ocamlx(NCoq_Init_Nat)
  • ocamlx(NCoq_Init_Notations)
  • ocamlx(NCoq_Init_Number)
  • ocamlx(NCoq_Init_Peano)
  • ocamlx(NCoq_Init_Prelude)
  • ocamlx(NCoq_Init_Specif)
  • ocamlx(NCoq_Init_Tactics)
  • ocamlx(NCoq_Init_Tauto)
  • ocamlx(NCoq_Init_Wf)
  • ocamlx(NCoq_Lists_List)
  • ocamlx(NCoq_Lists_ListDec)
  • ocamlx(NCoq_Lists_ListSet)
  • ocamlx(NCoq_Lists_ListTactics)
  • ocamlx(NCoq_Lists_SetoidList)
  • ocamlx(NCoq_Lists_SetoidPermutation)
  • ocamlx(NCoq_Lists_StreamMemo)
  • ocamlx(NCoq_Lists_Streams)
  • ocamlx(NCoq_Logic_Adjointification)
  • ocamlx(NCoq_Logic_Berardi)
  • ocamlx(NCoq_Logic_ChoiceFacts)
  • ocamlx(NCoq_Logic_Classical)
  • ocamlx(NCoq_Logic_ClassicalChoice)
  • ocamlx(NCoq_Logic_ClassicalDescription)
  • ocamlx(NCoq_Logic_ClassicalEpsilon)
  • ocamlx(NCoq_Logic_ClassicalFacts)
  • ocamlx(NCoq_Logic_ClassicalUniqueChoice)
  • ocamlx(NCoq_Logic_Classical_Pred_Type)
  • ocamlx(NCoq_Logic_Classical_Prop)
  • ocamlx(NCoq_Logic_ConstructiveEpsilon)
  • ocamlx(NCoq_Logic_Decidable)
  • ocamlx(NCoq_Logic_Description)
  • ocamlx(NCoq_Logic_Diaconescu)
  • ocamlx(NCoq_Logic_Epsilon)
  • ocamlx(NCoq_Logic_Eqdep)
  • ocamlx(NCoq_Logic_EqdepFacts)
  • ocamlx(NCoq_Logic_Eqdep_dec)
  • ocamlx(NCoq_Logic_ExtensionalFunctionRepresentative)
  • ocamlx(NCoq_Logic_ExtensionalityFacts)
  • ocamlx(NCoq_Logic_FinFun)
  • ocamlx(NCoq_Logic_FunctionalExtensionality)
  • ocamlx(NCoq_Logic_HLevels)
  • ocamlx(NCoq_Logic_Hurkens)
  • ocamlx(NCoq_Logic_IndefiniteDescription)
  • ocamlx(NCoq_Logic_JMeq)
  • ocamlx(NCoq_Logic_ProofIrrelevance)
  • ocamlx(NCoq_Logic_ProofIrrelevanceFacts)
  • ocamlx(NCoq_Logic_PropExtensionality)
  • ocamlx(NCoq_Logic_PropExtensionalityFacts)
  • ocamlx(NCoq_Logic_PropFacts)
  • ocamlx(NCoq_Logic_RelationalChoice)
  • ocamlx(NCoq_Logic_SetIsType)
  • ocamlx(NCoq_Logic_SetoidChoice)
  • ocamlx(NCoq_Logic_StrictProp)
  • ocamlx(NCoq_Logic_WKL)
  • ocamlx(NCoq_Logic_WeakFan)
  • ocamlx(NCoq_MSets_MSetAVL)
  • ocamlx(NCoq_MSets_MSetDecide)
  • ocamlx(NCoq_MSets_MSetEqProperties)
  • ocamlx(NCoq_MSets_MSetFacts)
  • ocamlx(NCoq_MSets_MSetGenTree)
  • ocamlx(NCoq_MSets_MSetInterface)
  • ocamlx(NCoq_MSets_MSetList)
  • ocamlx(NCoq_MSets_MSetPositive)
  • ocamlx(NCoq_MSets_MSetProperties)
  • ocamlx(NCoq_MSets_MSetRBT)
  • ocamlx(NCoq_MSets_MSetToFiniteSet)
  • ocamlx(NCoq_MSets_MSetWeakList)
  • ocamlx(NCoq_MSets_MSets)
  • ocamlx(NCoq_NArith_BinNat)
  • ocamlx(NCoq_NArith_BinNatDef)
  • ocamlx(NCoq_NArith_NArith)
  • ocamlx(NCoq_NArith_Ndec)
  • ocamlx(NCoq_NArith_Ndigits)
  • ocamlx(NCoq_NArith_Ndist)
  • ocamlx(NCoq_NArith_Ndiv_def)
  • ocamlx(NCoq_NArith_Ngcd_def)
  • ocamlx(NCoq_NArith_Nnat)
  • ocamlx(NCoq_NArith_Nsqrt_def)
  • ocamlx(NCoq_Numbers_AltBinNotations)
  • ocamlx(NCoq_Numbers_BinNums)
  • ocamlx(NCoq_Numbers_Cyclic_Abstract_CarryType)
  • ocamlx(NCoq_Numbers_Cyclic_Abstract_CyclicAxioms)
  • ocamlx(NCoq_Numbers_Cyclic_Abstract_DoubleType)
  • ocamlx(NCoq_Numbers_Cyclic_Abstract_NZCyclic)
  • ocamlx(NCoq_Numbers_Cyclic_Int31_Cyclic31)
  • ocamlx(NCoq_Numbers_Cyclic_Int31_Int31)
  • ocamlx(NCoq_Numbers_Cyclic_Int31_Ring31)
  • ocamlx(NCoq_Numbers_Cyclic_Int63_Cyclic63)
  • ocamlx(NCoq_Numbers_Cyclic_Int63_PrimInt63)
  • ocamlx(NCoq_Numbers_Cyclic_Int63_Ring63)
  • ocamlx(NCoq_Numbers_Cyclic_Int63_Sint63)
  • ocamlx(NCoq_Numbers_Cyclic_Int63_Uint63)
  • ocamlx(NCoq_Numbers_Cyclic_ZModulo_ZModulo)
  • ocamlx(NCoq_Numbers_DecimalFacts)
  • ocamlx(NCoq_Numbers_DecimalN)
  • ocamlx(NCoq_Numbers_DecimalNat)
  • ocamlx(NCoq_Numbers_DecimalPos)
  • ocamlx(NCoq_Numbers_DecimalQ)
  • ocamlx(NCoq_Numbers_DecimalR)
  • ocamlx(NCoq_Numbers_DecimalString)
  • ocamlx(NCoq_Numbers_DecimalZ)
  • ocamlx(NCoq_Numbers_HexadecimalFacts)
  • ocamlx(NCoq_Numbers_HexadecimalN)
  • ocamlx(NCoq_Numbers_HexadecimalNat)
  • ocamlx(NCoq_Numbers_HexadecimalPos)
  • ocamlx(NCoq_Numbers_HexadecimalQ)
  • ocamlx(NCoq_Numbers_HexadecimalR)
  • ocamlx(NCoq_Numbers_HexadecimalString)
  • ocamlx(NCoq_Numbers_HexadecimalZ)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZAdd)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZAddOrder)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZAxioms)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZBase)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZBits)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZDivEucl)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZDivFloor)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZDivTrunc)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZGcd)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZLcm)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZLt)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZMaxMin)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZMul)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZMulOrder)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZParity)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZPow)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZProperties)
  • ocamlx(NCoq_Numbers_Integer_Abstract_ZSgnAbs)
  • ocamlx(NCoq_Numbers_Integer_Binary_ZBinary)
  • ocamlx(NCoq_Numbers_Integer_NatPairs_ZNatPairs)
  • ocamlx(NCoq_Numbers_NaryFunctions)
  • ocamlx(NCoq_Numbers_NatInt_NZAdd)
  • ocamlx(NCoq_Numbers_NatInt_NZAddOrder)
  • ocamlx(NCoq_Numbers_NatInt_NZAxioms)
  • ocamlx(NCoq_Numbers_NatInt_NZBase)
  • ocamlx(NCoq_Numbers_NatInt_NZBits)
  • ocamlx(NCoq_Numbers_NatInt_NZDiv)
  • ocamlx(NCoq_Numbers_NatInt_NZDomain)
  • ocamlx(NCoq_Numbers_NatInt_NZGcd)
  • ocamlx(NCoq_Numbers_NatInt_NZLog)
  • ocamlx(NCoq_Numbers_NatInt_NZMul)
  • ocamlx(NCoq_Numbers_NatInt_NZMulOrder)
  • ocamlx(NCoq_Numbers_NatInt_NZOrder)
  • ocamlx(NCoq_Numbers_NatInt_NZParity)
  • ocamlx(NCoq_Numbers_NatInt_NZPow)
  • ocamlx(NCoq_Numbers_NatInt_NZProperties)
  • ocamlx(NCoq_Numbers_NatInt_NZSqrt)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NAdd)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NAddOrder)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NAxioms)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NBase)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NBits)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NDefOps)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NDiv)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NGcd)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NIso)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NLcm)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NLog)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NMaxMin)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NMulOrder)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NOrder)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NParity)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NPow)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NProperties)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NSqrt)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NStrongRec)
  • ocamlx(NCoq_Numbers_Natural_Abstract_NSub)
  • ocamlx(NCoq_Numbers_Natural_Binary_NBinary)
  • ocamlx(NCoq_Numbers_Natural_Peano_NPeano)
  • ocamlx(NCoq_Numbers_NumPrelude)
  • ocamlx(NCoq_PArith_BinPos)
  • ocamlx(NCoq_PArith_BinPosDef)
  • ocamlx(NCoq_PArith_PArith)
  • ocamlx(NCoq_PArith_POrderedType)
  • ocamlx(NCoq_PArith_Pnat)
  • ocamlx(NCoq_Program_Basics)
  • ocamlx(NCoq_Program_Combinators)
  • ocamlx(NCoq_Program_Equality)
  • ocamlx(NCoq_Program_Program)
  • ocamlx(NCoq_Program_Subset)
  • ocamlx(NCoq_Program_Syntax)
  • ocamlx(NCoq_Program_Tactics)
  • ocamlx(NCoq_Program_Utils)
  • ocamlx(NCoq_Program_Wf)
  • ocamlx(NCoq_QArith_QArith)
  • ocamlx(NCoq_QArith_QArith_base)
  • ocamlx(NCoq_QArith_QOrderedType)
  • ocamlx(NCoq_QArith_Qabs)
  • ocamlx(NCoq_QArith_Qcabs)
  • ocamlx(NCoq_QArith_Qcanon)
  • ocamlx(NCoq_QArith_Qfield)
  • ocamlx(NCoq_QArith_Qminmax)
  • ocamlx(NCoq_QArith_Qpower)
  • ocamlx(NCoq_QArith_Qreals)
  • ocamlx(NCoq_QArith_Qreduction)
  • ocamlx(NCoq_QArith_Qring)
  • ocamlx(NCoq_QArith_Qround)
  • ocamlx(NCoq_Reals_Abstract_ConstructiveAbs)
  • ocamlx(NCoq_Reals_Abstract_ConstructiveLUB)
  • ocamlx(NCoq_Reals_Abstract_ConstructiveLimits)
  • ocamlx(NCoq_Reals_Abstract_ConstructiveMinMax)
  • ocamlx(NCoq_Reals_Abstract_ConstructivePower)
  • ocamlx(NCoq_Reals_Abstract_ConstructiveReals)
  • ocamlx(NCoq_Reals_Abstract_ConstructiveRealsMorphisms)
  • ocamlx(NCoq_Reals_Abstract_ConstructiveSum)
  • ocamlx(NCoq_Reals_Alembert)
  • ocamlx(NCoq_Reals_AltSeries)
  • ocamlx(NCoq_Reals_ArithProp)
  • ocamlx(NCoq_Reals_Binomial)
  • ocamlx(NCoq_Reals_Cauchy_ConstructiveCauchyAbs)
  • ocamlx(NCoq_Reals_Cauchy_ConstructiveCauchyReals)
  • ocamlx(NCoq_Reals_Cauchy_ConstructiveCauchyRealsMult)
  • ocamlx(NCoq_Reals_Cauchy_ConstructiveExtra)
  • ocamlx(NCoq_Reals_Cauchy_ConstructiveRcomplete)
  • ocamlx(NCoq_Reals_Cauchy_PosExtra)
  • ocamlx(NCoq_Reals_Cauchy_QExtra)
  • ocamlx(NCoq_Reals_Cauchy_prod)
  • ocamlx(NCoq_Reals_ClassicalConstructiveReals)
  • ocamlx(NCoq_Reals_ClassicalDedekindReals)
  • ocamlx(NCoq_Reals_Cos_plus)
  • ocamlx(NCoq_Reals_Cos_rel)
  • ocamlx(NCoq_Reals_DiscrR)
  • ocamlx(NCoq_Reals_Exp_prop)
  • ocamlx(NCoq_Reals_Integration)
  • ocamlx(NCoq_Reals_MVT)
  • ocamlx(NCoq_Reals_Machin)
  • ocamlx(NCoq_Reals_NewtonInt)
  • ocamlx(NCoq_Reals_PSeries_reg)
  • ocamlx(NCoq_Reals_PartSum)
  • ocamlx(NCoq_Reals_RIneq)
  • ocamlx(NCoq_Reals_RList)
  • ocamlx(NCoq_Reals_ROrderedType)
  • ocamlx(NCoq_Reals_R_Ifp)
  • ocamlx(NCoq_Reals_R_sqr)
  • ocamlx(NCoq_Reals_R_sqrt)
  • ocamlx(NCoq_Reals_Ranalysis)
  • ocamlx(NCoq_Reals_Ranalysis1)
  • ocamlx(NCoq_Reals_Ranalysis2)
  • ocamlx(NCoq_Reals_Ranalysis3)
  • ocamlx(NCoq_Reals_Ranalysis4)
  • ocamlx(NCoq_Reals_Ranalysis5)
  • ocamlx(NCoq_Reals_Ranalysis_reg)
  • ocamlx(NCoq_Reals_Ratan)
  • ocamlx(NCoq_Reals_Raxioms)
  • ocamlx(NCoq_Reals_Rbase)
  • ocamlx(NCoq_Reals_Rbasic_fun)
  • ocamlx(NCoq_Reals_Rcomplete)
  • ocamlx(NCoq_Reals_Rdefinitions)
  • ocamlx(NCoq_Reals_Rderiv)
  • ocamlx(NCoq_Reals_Reals)
  • ocamlx(NCoq_Reals_Rfunctions)
  • ocamlx(NCoq_Reals_Rgeom)
  • ocamlx(NCoq_Reals_RiemannInt)
  • ocamlx(NCoq_Reals_RiemannInt_SF)
  • ocamlx(NCoq_Reals_Rlimit)
  • ocamlx(NCoq_Reals_Rlogic)
  • ocamlx(NCoq_Reals_Rminmax)
  • ocamlx(NCoq_Reals_Rpow_def)
  • ocamlx(NCoq_Reals_Rpower)
  • ocamlx(NCoq_Reals_Rprod)
  • ocamlx(NCoq_Reals_Rregisternames)
  • ocamlx(NCoq_Reals_Rseries)
  • ocamlx(NCoq_Reals_Rsigma)
  • ocamlx(NCoq_Reals_Rsqrt_def)
  • ocamlx(NCoq_Reals_Rtopology)
  • ocamlx(NCoq_Reals_Rtrigo)
  • ocamlx(NCoq_Reals_Rtrigo1)
  • ocamlx(NCoq_Reals_Rtrigo_alt)
  • ocamlx(NCoq_Reals_Rtrigo_calc)
  • ocamlx(NCoq_Reals_Rtrigo_def)
  • ocamlx(NCoq_Reals_Rtrigo_facts)
  • ocamlx(NCoq_Reals_Rtrigo_fun)
  • ocamlx(NCoq_Reals_Rtrigo_reg)
  • ocamlx(NCoq_Reals_Runcountable)
  • ocamlx(NCoq_Reals_SeqProp)
  • ocamlx(NCoq_Reals_SeqSeries)
  • ocamlx(NCoq_Reals_SplitAbsolu)
  • ocamlx(NCoq_Reals_SplitRmult)
  • ocamlx(NCoq_Reals_Sqrt_reg)
  • ocamlx(NCoq_Relations_Operators_Properties)
  • ocamlx(NCoq_Relations_Relation_Definitions)
  • ocamlx(NCoq_Relations_Relation_Operators)
  • ocamlx(NCoq_Relations_Relations)
  • ocamlx(NCoq_Setoids_Setoid)
  • ocamlx(NCoq_Sets_Classical_sets)
  • ocamlx(NCoq_Sets_Constructive_sets)
  • ocamlx(NCoq_Sets_Cpo)
  • ocamlx(NCoq_Sets_Ensembles)
  • ocamlx(NCoq_Sets_Finite_sets)
  • ocamlx(NCoq_Sets_Finite_sets_facts)
  • ocamlx(NCoq_Sets_Image)
  • ocamlx(NCoq_Sets_Infinite_sets)
  • ocamlx(NCoq_Sets_Integers)
  • ocamlx(NCoq_Sets_Multiset)
  • ocamlx(NCoq_Sets_Partial_Order)
  • ocamlx(NCoq_Sets_Permut)
  • ocamlx(NCoq_Sets_Powerset)
  • ocamlx(NCoq_Sets_Powerset_Classical_facts)
  • ocamlx(NCoq_Sets_Powerset_facts)
  • ocamlx(NCoq_Sets_Relations_1)
  • ocamlx(NCoq_Sets_Relations_1_facts)
  • ocamlx(NCoq_Sets_Relations_2)
  • ocamlx(NCoq_Sets_Relations_2_facts)
  • ocamlx(NCoq_Sets_Relations_3)
  • ocamlx(NCoq_Sets_Relations_3_facts)
  • ocamlx(NCoq_Sets_Uniset)
  • ocamlx(NCoq_Sorting_CPermutation)
  • ocamlx(NCoq_Sorting_Heap)
  • ocamlx(NCoq_Sorting_Mergesort)
  • ocamlx(NCoq_Sorting_PermutEq)
  • ocamlx(NCoq_Sorting_PermutSetoid)
  • ocamlx(NCoq_Sorting_Permutation)
  • ocamlx(NCoq_Sorting_Sorted)
  • ocamlx(NCoq_Sorting_Sorting)
  • ocamlx(NCoq_Strings_Ascii)
  • ocamlx(NCoq_Strings_BinaryString)
  • ocamlx(NCoq_Strings_Byte)
  • ocamlx(NCoq_Strings_ByteVector)
  • ocamlx(NCoq_Strings_HexString)
  • ocamlx(NCoq_Strings_OctalString)
  • ocamlx(NCoq_Strings_String)
  • ocamlx(NCoq_Structures_DecidableType)
  • ocamlx(NCoq_Structures_DecidableTypeEx)
  • ocamlx(NCoq_Structures_Equalities)
  • ocamlx(NCoq_Structures_EqualitiesFacts)
  • ocamlx(NCoq_Structures_GenericMinMax)
  • ocamlx(NCoq_Structures_OrderedType)
  • ocamlx(NCoq_Structures_OrderedTypeAlt)
  • ocamlx(NCoq_Structures_OrderedTypeEx)
  • ocamlx(NCoq_Structures_Orders)
  • ocamlx(NCoq_Structures_OrdersAlt)
  • ocamlx(NCoq_Structures_OrdersEx)
  • ocamlx(NCoq_Structures_OrdersFacts)
  • ocamlx(NCoq_Structures_OrdersLists)
  • ocamlx(NCoq_Structures_OrdersTac)
  • ocamlx(NCoq_Unicode_Utf8)
  • ocamlx(NCoq_Unicode_Utf8_core)
  • ocamlx(NCoq_Vectors_Fin)
  • ocamlx(NCoq_Vectors_Vector)
  • ocamlx(NCoq_Vectors_VectorDef)
  • ocamlx(NCoq_Vectors_VectorEq)
  • ocamlx(NCoq_Vectors_VectorSpec)
  • ocamlx(NCoq_Wellfounded_Disjoint_Union)
  • ocamlx(NCoq_Wellfounded_Inclusion)
  • ocamlx(NCoq_Wellfounded_Inverse_Image)
  • ocamlx(NCoq_Wellfounded_Lexicographic_Exponentiation)
  • ocamlx(NCoq_Wellfounded_Lexicographic_Product)
  • ocamlx(NCoq_Wellfounded_Transitive_Closure)
  • ocamlx(NCoq_Wellfounded_Union)
  • ocamlx(NCoq_Wellfounded_Well_Ordering)
  • ocamlx(NCoq_Wellfounded_Wellfounded)
  • ocamlx(NCoq_ZArith_BinInt)
  • ocamlx(NCoq_ZArith_BinIntDef)
  • ocamlx(NCoq_ZArith_Int)
  • ocamlx(NCoq_ZArith_Wf_Z)
  • ocamlx(NCoq_ZArith_ZArith)
  • ocamlx(NCoq_ZArith_ZArith_base)
  • ocamlx(NCoq_ZArith_ZArith_dec)
  • ocamlx(NCoq_ZArith_Zabs)
  • ocamlx(NCoq_ZArith_Zbool)
  • ocamlx(NCoq_ZArith_Zcompare)
  • ocamlx(NCoq_ZArith_Zcomplements)
  • ocamlx(NCoq_ZArith_Zdigits)
  • ocamlx(NCoq_ZArith_Zdiv)
  • ocamlx(NCoq_ZArith_Zeuclid)
  • ocamlx(NCoq_ZArith_Zeven)
  • ocamlx(NCoq_ZArith_Zgcd_alt)
  • ocamlx(NCoq_ZArith_Zhints)
  • ocamlx(NCoq_ZArith_Zmax)
  • ocamlx(NCoq_ZArith_Zmin)
  • ocamlx(NCoq_ZArith_Zminmax)
  • ocamlx(NCoq_ZArith_Zmisc)
  • ocamlx(NCoq_ZArith_Znat)
  • ocamlx(NCoq_ZArith_Znumtheory)
  • ocamlx(NCoq_ZArith_Zorder)
  • ocamlx(NCoq_ZArith_Zpow_alt)
  • ocamlx(NCoq_ZArith_Zpow_def)
  • ocamlx(NCoq_ZArith_Zpow_facts)
  • ocamlx(NCoq_ZArith_Zpower)
  • ocamlx(NCoq_ZArith_Zquot)
  • ocamlx(NCoq_ZArith_Zwf)
  • ocamlx(NCoq_ZArith_auxiliary)
  • ocamlx(NCoq_btauto_Algebra)
  • ocamlx(NCoq_btauto_Btauto)
  • ocamlx(NCoq_btauto_Reflect)
  • ocamlx(NCoq_derive_Derive)
  • ocamlx(NCoq_extraction_ExtrHaskellBasic)
  • ocamlx(NCoq_extraction_ExtrHaskellNatInt)
  • ocamlx(NCoq_extraction_ExtrHaskellNatInteger)
  • ocamlx(NCoq_extraction_ExtrHaskellNatNum)
  • ocamlx(NCoq_extraction_ExtrHaskellString)
  • ocamlx(NCoq_extraction_ExtrHaskellZInt)
  • ocamlx(NCoq_extraction_ExtrHaskellZInteger)
  • ocamlx(NCoq_extraction_ExtrHaskellZNum)
  • ocamlx(NCoq_extraction_ExtrOCamlFloats)
  • ocamlx(NCoq_extraction_ExtrOCamlInt63)
  • ocamlx(NCoq_extraction_ExtrOCamlPArray)
  • ocamlx(NCoq_extraction_ExtrOcamlBasic)
  • ocamlx(NCoq_extraction_ExtrOcamlChar)
  • ocamlx(NCoq_extraction_ExtrOcamlIntConv)
  • ocamlx(NCoq_extraction_ExtrOcamlNatBigInt)
  • ocamlx(NCoq_extraction_ExtrOcamlNatInt)
  • ocamlx(NCoq_extraction_ExtrOcamlNativeString)
  • ocamlx(NCoq_extraction_ExtrOcamlString)
  • ocamlx(NCoq_extraction_ExtrOcamlZBigInt)
  • ocamlx(NCoq_extraction_ExtrOcamlZInt)
  • ocamlx(NCoq_extraction_Extraction)
  • ocamlx(NCoq_funind_FunInd)
  • ocamlx(NCoq_funind_Recdef)
  • ocamlx(NCoq_micromega_DeclConstant)
  • ocamlx(NCoq_micromega_Env)
  • ocamlx(NCoq_micromega_EnvRing)
  • ocamlx(NCoq_micromega_Fourier)
  • ocamlx(NCoq_micromega_Fourier_util)
  • ocamlx(NCoq_micromega_Lia)
  • ocamlx(NCoq_micromega_Lqa)
  • ocamlx(NCoq_micromega_Lra)
  • ocamlx(NCoq_micromega_MExtraction)
  • ocamlx(NCoq_micromega_OrderedRing)
  • ocamlx(NCoq_micromega_Psatz)
  • ocamlx(NCoq_micromega_QMicromega)
  • ocamlx(NCoq_micromega_RMicromega)
  • ocamlx(NCoq_micromega_Refl)
  • ocamlx(NCoq_micromega_RingMicromega)
  • ocamlx(NCoq_micromega_Tauto)
  • ocamlx(NCoq_micromega_VarMap)
  • ocamlx(NCoq_micromega_ZArith_hints)
  • ocamlx(NCoq_micromega_ZCoeff)
  • ocamlx(NCoq_micromega_ZMicromega)
  • ocamlx(NCoq_micromega_Zify)
  • ocamlx(NCoq_micromega_ZifyBool)
  • ocamlx(NCoq_micromega_ZifyClasses)
  • ocamlx(NCoq_micromega_ZifyComparison)
  • ocamlx(NCoq_micromega_ZifyInst)
  • ocamlx(NCoq_micromega_ZifyN)
  • ocamlx(NCoq_micromega_ZifyNat)
  • ocamlx(NCoq_micromega_ZifyPow)
  • ocamlx(NCoq_micromega_ZifySint63)
  • ocamlx(NCoq_micromega_ZifyUint63)
  • ocamlx(NCoq_micromega_Ztac)
  • ocamlx(NCoq_nsatz_Nsatz)
  • ocamlx(NCoq_nsatz_NsatzTactic)
  • ocamlx(NCoq_omega_OmegaLemmas)
  • ocamlx(NCoq_omega_PreOmega)
  • ocamlx(NCoq_rtauto_Bintree)
  • ocamlx(NCoq_rtauto_Rtauto)
  • ocamlx(NCoq_setoid_ring_Algebra_syntax)
  • ocamlx(NCoq_setoid_ring_ArithRing)
  • ocamlx(NCoq_setoid_ring_BinList)
  • ocamlx(NCoq_setoid_ring_Cring)
  • ocamlx(NCoq_setoid_ring_Field)
  • ocamlx(NCoq_setoid_ring_Field_tac)
  • ocamlx(NCoq_setoid_ring_Field_theory)
  • ocamlx(NCoq_setoid_ring_InitialRing)
  • ocamlx(NCoq_setoid_ring_Integral_domain)
  • ocamlx(NCoq_setoid_ring_NArithRing)
  • ocamlx(NCoq_setoid_ring_Ncring)
  • ocamlx(NCoq_setoid_ring_Ncring_initial)
  • ocamlx(NCoq_setoid_ring_Ncring_polynom)
  • ocamlx(NCoq_setoid_ring_Ncring_tac)
  • ocamlx(NCoq_setoid_ring_RealField)
  • ocamlx(NCoq_setoid_ring_Ring)
  • ocamlx(NCoq_setoid_ring_Ring_base)
  • ocamlx(NCoq_setoid_ring_Ring_polynom)
  • ocamlx(NCoq_setoid_ring_Ring_tac)
  • ocamlx(NCoq_setoid_ring_Ring_theory)
  • ocamlx(NCoq_setoid_ring_Rings_Q)
  • ocamlx(NCoq_setoid_ring_Rings_R)
  • ocamlx(NCoq_setoid_ring_Rings_Z)
  • ocamlx(NCoq_setoid_ring_ZArithRing)
  • ocamlx(NCoq_ssr_ssrbool)
  • ocamlx(NCoq_ssr_ssrclasses)
  • ocamlx(NCoq_ssr_ssreflect)
  • ocamlx(NCoq_ssr_ssrfun)
  • ocamlx(NCoq_ssr_ssrsetoid)
  • ocamlx(NCoq_ssr_ssrunder)
  • ocamlx(NCoq_ssrmatching_ssrmatching)
  • ocamlx(NLtac2_Array)
  • ocamlx(NLtac2_Bool)
  • ocamlx(NLtac2_Char)
  • ocamlx(NLtac2_Constr)
  • ocamlx(NLtac2_Control)
  • ocamlx(NLtac2_Env)
  • ocamlx(NLtac2_Fresh)
  • ocamlx(NLtac2_Ident)
  • ocamlx(NLtac2_Ind)
  • ocamlx(NLtac2_Init)
  • ocamlx(NLtac2_Int)
  • ocamlx(NLtac2_List)
  • ocamlx(NLtac2_Ltac1)
  • ocamlx(NLtac2_Ltac2)
  • ocamlx(NLtac2_Message)
  • ocamlx(NLtac2_Notations)
  • ocamlx(NLtac2_Option)
  • ocamlx(NLtac2_Pattern)
  • ocamlx(NLtac2_Printf)
  • ocamlx(NLtac2_Std)
  • ocamlx(NLtac2_String)

Files


Sources on Pagure