aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-06-16Use a smart map_constrAmin Timany
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Move (part of) tests from checker to successAmin Timany
2017-06-16Remove Warnings: unused value ...Amin Timany
2017-06-16Checker add test for non-trivial constraintsAmin Timany
2017-06-16Properly instantiate contexts before pushingAmin Timany
2017-06-16Enable the checking of ind subtyping in checkerAmin Timany
2017-06-16Document cumulativity for inductive typesAmin Timany
2017-06-16Change the option to Set Inductive CumulativityAmin Timany
2017-06-16Add printing of cumulativity in inductive typesAmin Timany
2017-06-16Move univops from kernel to libraryAmin Timany
2017-06-16Correct coqchk checking subtyping relation for inductivesAmin Timany
2017-06-16Correct coqchk reductionAmin Timany
2017-06-16Simplify Univ.mlAmin Timany
2017-06-16Fix a bugAmin Timany
2017-06-16Disable debug printingAmin Timany
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-16Fix bugsAmin Timany
2017-06-16Squashed commit of the following:Amin Timany
2017-06-16Make unification use subtyping info of inductivesAmin Timany
2017-06-16Fix cum/conv for inductive typesAmin Timany
2017-06-16Use inductive subtyping for conv/cumulAmin Timany
2017-06-16Change the place of inference after sect dischargeAmin Timany
2017-06-16Subtyping inference for inductoves and recordsAmin Timany
2017-06-16Add subtyping inference for inductive typesAmin Timany
2017-06-16Correct subtyping check for constructorsAmin Timany
2017-06-16Fix typo in error messageAmin Timany
2017-06-16Check subtyping of inductive types in KernelAmin Timany
2017-06-16Using UInfoInd for universes in inductive typesAmin Timany
2017-06-16New datastructure for universes of inductive typesAmin Timany
2017-06-16Extend definition of inductives to include subtyping infoAmin Timany
2017-06-15Move TIMER to right in front of COQCJason Gross
2017-06-15Fix `make TIMED=1` garbageJason Gross
2017-06-15Strip trailing whitespaceJason Gross
2017-06-15Merge PR#741: Fix documentation of Typeclasses eauto :=Maxime Dénès
2017-06-15Merge PR#713: Bump year in headers.Maxime Dénès
2017-06-15Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraintsMaxime Dénès
2017-06-15Merge PR#752: Adding a test case as requested in bug 5205.Maxime Dénès
2017-06-15Merge PR#747: Fix Bug #5568, no dup notation warnings on repeated module importsMaxime Dénès
2017-06-15Merge PR#748: [stm] More fixes for nested commands [bugzilla 5589]Maxime Dénès
2017-06-15Merge PR#778: Revert "[travis] temporary UniMath overlay"Maxime Dénès
2017-06-15Merge PR#719: Constrexpr.Numeral without bigintMaxime Dénès
2017-06-15Merge PR#769: [lib] Remove obsolete state-management function add_frozen_stateMaxime Dénès
2017-06-15fix dev/base_include (thanks Zimmi48)Pierre Letouzey
2017-06-15Remove ci-fiat-parsers from allowed_failuresJason Gross
2017-06-15Update fiat-parsers overlayJason Gross
2017-06-15API: Hints.run_hint,Pfedit.current_proof_statementJason Gross
2017-06-15Makefile.build : restore (temporarily?) the anti-cmi-corruption hacksPierre Letouzey
2017-06-15plugins/ltac : avoid spurious .cmxs filesPierre Letouzey
2017-06-15Merge PR#375: DeprecationMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-17 13:32:08 +0000