aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
2017-11-22Add test-suite tests for timing scriptsJason Gross
2017-11-22allow whitespace around infix opPaul Steckler
2017-11-22use OCaml criteria for infix ops, #6212Paul Steckler
2017-11-22Fix universe polymorphic Program obligations.Matthieu Sozeau
2017-11-21Merge PR #6178: Have the coq_makefile timing test-suite print moreMaxime Dénès
2017-11-21Merge PR #6113: Extra work on ltac printing: fixing #5787, some parenthesesMaxime Dénès
2017-11-20Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Hugo Herbelin
2017-11-20Fixing factorization of recursive notations in the case of an atomic separator.Hugo Herbelin
2017-11-20Merge PR #6166: Fix regression in treating Defined as definedMaxime Dénès
2017-11-20Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...Maxime Dénès
2017-11-20Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces unbo...Maxime Dénès
2017-11-19Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gaëtan Gilbert
2017-11-17Have the coq_makefile timing test-suite print moreJason Gross
2017-11-16Merge PR #6132: Fixes #6129 (declaration of coercions made compatible with lo...Maxime Dénès
2017-11-16Merge PR #6104: Fixing encoding in coqdoc output tests.Maxime Dénès
2017-11-15Fix regression in treating Defined as definedTej Chajed
2017-11-15Fix #5761: cbv on undefined evars under binders produces unbound relGaëtan Gilbert
2017-11-15Merge PR #6122: Remove dependency of test-suite on git (fix #5725).Maxime Dénès
2017-11-15Fix test-suite.Robbert Krebbers
2017-11-14Fixes #6129 (declaration of coercions made compatible with local definitions).Hugo Herbelin
2017-11-14One more step in fixing #5762 ("where" clause).Hugo Herbelin
2017-11-13Fixing encoding in coqdoc output tests.Hugo Herbelin
2017-11-13Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac.Maxime Dénès
2017-11-09Introduce default.nix for Nix users.Théo Zimmermann
2017-11-08Fixing a remaining "coqdoc" problem with bug #5762 and pr #1120.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-06 18:10:05 +0000