aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2020-03-26Fix #11845: anomaly when including partially applied functorGaëtan Gilbert
2020-03-26Merge PR #11891: Fix levels of `<=?` and `<?` in the stdlibHugo Herbelin
2020-03-23Fix levels of `<=?` and `<?` in the stdlibJason Gross
2020-03-22Testing notations which are specific numerals.Hugo Herbelin
2020-03-22Adding a test for printing single characters.Hugo Herbelin
2020-03-22Test-suite: Assume coqtop output is text even with non-printable characters.Hugo Herbelin
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
2020-03-20Merge PR #11814: Document coq_makefile behavior wrt -native-compiler yesEnrico Tassi
2020-03-20Merge PR #11847: Properly thread let-bindings in Funind principle construction.Pierre Courtieu
2020-03-19Interpret the Export modifier of Set and Unset as an attribute.Théo Zimmermann
2020-03-19Merge PR #11760: firstorder: default tactic is “auto with core”Théo Zimmermann
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
2020-03-19Merge PR #11822: Grants #11692: clear dependent knows about let-inPierre-Marie Pédrot
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-18Adding a round-trip test for binders.Pierre-Marie Pédrot
2020-03-18Actually use the binder type for Ltac2 that should be used in the kernel.Pierre-Marie Pédrot
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-18Export the user-facing attribute for hint locality.Pierre-Marie Pédrot
2020-03-18Change some ouput tests due to the printing of implicitsSimonBoulier
2020-03-17Properly thread let-bindings in Funind principle construction.Pierre-Marie Pédrot
2020-03-17Merge PR #11811: Remove a positivity check when Positivity Checking is offGaëtan Gilbert
2020-03-17Add test for PR11811 (disable a positivity check)SimonBoulier
2020-03-16Document coq_makefile behavior wrt -native-compiler yesPierre Roux
2020-03-16Fix coq-makefile/native1 testPierre Roux
2020-03-14Fixes #11692 (clear dependent knows about let-in).Hugo Herbelin
2020-03-14Merge PR #10858: Implementing postponed constraints in TC resolutionGaëtan Gilbert
2020-03-13Implementing postponed constraints in TC resolutionMatthieu Sozeau
2020-03-12Merge PR #11798: Tests make bytecodeEnrico Tassi
2020-03-11Merge PR #11769: Fix #9930: "change" replaces 0-param projections by constantsPierre-Marie Pédrot
2020-03-11Merge PR #11786: Fix #11730: Mangle Names vs InfixPierre-Marie Pédrot
2020-03-10test coq-makefile/findlib-package-unpacked: only try to invoke 'make' whenRalf Treinen
2020-03-10test coq-makefile/camldep: try to build a cmx only when there is an ocamloptRalf Treinen
2020-03-10Fixing little bug in parsing decimal numbers in R.Hugo Herbelin
2020-03-09Fix #11730: Mangle Names vs InfixGaëtan Gilbert
2020-03-09Fix #9930: "change" replaces 0-param projections by constantsGaëtan Gilbert
2020-03-08Merge PR #11740: Ltac2: Add notation for enough and eenoughPierre-Marie Pédrot
2020-03-06Merge PR #11698: Fix #11592: Side effect safety may be broken by universe eff...Gaëtan Gilbert
2020-03-06Merge PR #11723: Fix mishandling of sigma in guess_elim (regression from 8.11)Pierre-Marie Pédrot
2020-03-06Adding a test to the test-suite.Pierre-Marie Pédrot
2020-03-05Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ...Pierre-Marie Pédrot
2020-03-05Merge PR #11602: Adding support for an "only parsing" modifier in "where"-bas...Pierre-Marie Pédrot
2020-03-04Merge PR #11715: Be robust in calculating visible ids for non-registered cons...Hugo Herbelin
2020-03-04Merge PR #11429: [zify] several efficiency enhancementsVincent Laporte
2020-03-04Adding support for an "only parsing" modifier in "where"-based notations.Hugo Herbelin
2020-03-03[loadpath] Rework and simplify ML loadpath handlingEmilio Jesus Gallego Arias
2020-03-03[zify] efficiency improvementsFrédéric Besson
2020-03-03Ltac2: Add notation for enough and eenoughMichael Soegtrop
2020-03-03Adding an alias "pose proof (x:=a)" for "pose proof a as x".Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 22:19:11 +0000