aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2017-12-11Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Maxime Dénès
2017-12-08Merge PR #6158: Allows a level in the raw and glob printersMaxime Dénès
2017-12-07Merge PR #873: New strategy based on open scopes for deciding which notation ...Maxime Dénès
2017-12-06Fix #6323: stronger restrict universe context vs abstract.Gaëtan Gilbert
2017-12-05Merge PR #890: Global universe declarationsMaxime Dénès
2017-12-05Merge PR #6306: Adding a test for #6304 (a bug with "fix" in notations).Maxime Dénès
2017-12-05Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212Maxime Dénès
2017-12-05Merge PR #6210: More complete not-fully-applied error messages, #6145Maxime Dénès
2017-12-03Adding a test for #6304 (bug with fix in notations).Hugo Herbelin
2017-12-01Cleanup API for registering universe binders.Matthieu Sozeau
2017-12-01Tests for global universe declarationsMatthieu Sozeau
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
2017-11-30Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ...Maxime Dénès
2017-11-30Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as in...Maxime Dénès
2017-11-29Merge PR #6253: Fixing inconsistent associativity of level 10 in the table of...Maxime Dénès
2017-11-28In injection/inversion, consider all template-polymorphic types as injectable.Hugo Herbelin
2017-11-28more complete not-fully-applied error messages, #6145Paul Steckler
2017-11-28Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gaëtan Gilbert
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-28Merge PR #6235: Fixing failing mkdir in test-suite for coq-makefile.Maxime Dénès
2017-11-27Selecting which notation to print based on current stack of scope.Hugo Herbelin
2017-11-27Pre-isolating a notation test to avoid interferences.Hugo Herbelin
2017-11-27Merge PR #6237: coq_makefile tests: build in easily removed temporary subdire...Maxime Dénès
2017-11-27Merge PR #6149: Update TimeFileMaker.py to correctly sort timing diffsMaxime Dénès
2017-11-27Fixing associativity registered for level 10.Hugo Herbelin
2017-11-25Restrict universe context when declaring constants in obligations.Gaëtan Gilbert
2017-11-25Fix #5347: unify declaration of axioms with and without bound univs.Gaëtan Gilbert
2017-11-25Fix interpretation of global universes in univdecl constraints.Gaëtan Gilbert
2017-11-25Forbid repeated names in universe binders.Gaëtan Gilbert
2017-11-25Universe binders survive sections, modules and compilation.Gaëtan Gilbert
2017-11-25Allow local universe renaming in Print.Gaëtan Gilbert
2017-11-25Make restrict_universe_context stronger.Gaëtan Gilbert
2017-11-24In close_proof only check univ decls with the restricted context.Gaëtan Gilbert
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
2017-11-24restrict_universe_context: do not prune named universes.Gaëtan Gilbert
2017-11-24Fix defining non primitive projections with abstracted universes.Gaëtan Gilbert
2017-11-24Stop exposing UState.universe_context and its Evd wrapper.Gaëtan Gilbert
2017-11-24Printing again "intros **" as "intros" by default.Hugo Herbelin
2017-11-24Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Hugo Herbelin
2017-11-24Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRingMaxime Dénès
2017-11-24Merge PR #876: In omega or romega, recognizing Z and nat modulo conversionMaxime Dénès
2017-11-24coq_makefile tests: build in easily removed temporary subdirectory.Gaëtan Gilbert
2017-11-24Fixing failing mkdir in test-suite for coq-makefile.Hugo Herbelin
2017-11-23Merge PR #6167: Fixing factorization of recursive notations with an atomic se...Maxime Dénès
2017-11-23Merge PR #6203: Fix universe polymorphic Program obligations.Maxime Dénès
2017-11-23Recognizing Z in romega up to conversion.Hugo Herbelin
2017-11-23Using is_conv rather than eq_constr to find `nat` or `Z` in omega.Hugo Herbelin
2017-11-23Fixing a 8.7 regression of ring_simplify in ArithRing.Hugo Herbelin
2017-11-23Merge PR #6123: Nix fileMaxime Dénès
2017-11-23Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 11:22:35 +0000