aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2020-07-23Hint Opaque/Transparent/Unfold: don't error on opaque constantsGaëtan Gilbert
2020-07-23Merge PR #12679: Remove redundant data from VM case switch.Gaëtan Gilbert
2020-07-23Merge PR #12698: Fixing mention of `unfold` as example of tactic taking a qua...Théo Zimmermann
2020-07-22Merge PR #12664: Turn various anomalies into regular errors in primitive decl...Pierre-Marie Pédrot
2020-07-22Remove redundant data from VM case switch.Pierre-Marie Pédrot
2020-07-21Turn various anomalies into regular errors in primitive declaration pathGaëtan Gilbert
2020-07-21Merge PR #12697: Fix bug #12691: an only-parsing notation needs to produce a ...Emilio Jesus Gallego Arias
2020-07-20Merge PR #12684: Do not print constructor and inductive types as terms when a...Gaëtan Gilbert
2020-07-17Add tests for the interpretation of "unfold".Hugo Herbelin
2020-07-17Merge PR #12683: Fixes #12682: printing bug with recursive notations for n-ar...Emilio Jesus Gallego Arias
2020-07-17Merge PR #12631: Fix record pattern interpretation with implicit argumentsEmilio Jesus Gallego Arias
2020-07-15Do not print global refs as terms when asked to be printed as themselves.Hugo Herbelin
2020-07-15Fix bug #12691 (an only parsing notation induces a generic printing format).Hugo Herbelin
2020-07-12Fixes #12682 (recursive notation printing bug with n-ary applications).Hugo Herbelin
2020-07-11Merge PR #12650: Recordops: unify struc_typ summary record and libobject entr...Pierre-Marie Pédrot
2020-07-11Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/nativePierre-Marie Pédrot
2020-07-10Merge PR #12666: Add test for #10890 derive vs abstractEmilio Jesus Gallego Arias
2020-07-10Merge PR #12537: Take into account the existing delta-resolver when starting ...Gaëtan Gilbert
2020-07-09Add test for #10890 derive vs abstractGaëtan Gilbert
2020-07-09Recordops: unify struc_typ summary record and libobject entry struc_tupleGaëtan Gilbert
2020-07-08Merge PR #12627: Fix Canonical with universe polymorphism and primitive proje...Enrico Tassi
2020-07-08Adding test for #12525 (Search of lemmas in Include failing when in Module).Hugo Herbelin
2020-07-08Merge PR #12652: Fix erroneous implicits-in-term warningEmilio Jesus Gallego Arias
2020-07-07Merge PR #12626: Fix Context with nonmaximplicit.Emilio Jesus Gallego Arias
2020-07-07Fix erroneous implicits-in-term warningGaëtan Gilbert
2020-07-06Merge PR #11604: Primitive persistent arraysPierre-Marie Pédrot
2020-07-06Correctly readback blocked CaseInvert matches in VM/nativeGaëtan Gilbert
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-05Fix Canonical with universe polymorphism and primitive projectionGaëtan Gilbert
2020-07-05Merge PR #12594: Fix ltac2 type parametersMichael Soegtrop
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
2020-07-02Fix record pattern interpretation with implicit argumentsGaëtan Gilbert
2020-07-02Fix Context with nonmaximplicit.Gaëtan Gilbert
2020-07-02Merge PR #12572: Correctly classify variables as being unfoldable in dnet pat...Gaëtan Gilbert
2020-07-01Add a test for Ltac2 parsing of parameterized types.Pierre-Marie Pédrot
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Merge PR #12605: [test-suite] async-proofs off in tests with Fail TimeoutGaëtan Gilbert
2020-06-30Merge PR #11977: Generate default names for bound universes of polymorphic de...Emilio Jesus Gallego Arias
2020-06-29[test-suite] async-proofs off in tests with Fail TimeoutEnrico Tassi
2020-06-29Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_listPierre-Marie Pédrot
2020-06-25Generate names for anonymous polymorphic universesGaëtan Gilbert
2020-06-24[test-suite] Fix dependencies of modules/ filesJason Gross
2020-06-24Merge PR #12532: Use the unification result for eauto's eapply.Matthieu Sozeau
2020-06-23Correctly classify variables as being unfoldable in dnet patterns.Pierre-Marie Pédrot
2020-06-23Merge PR #12530: Fix glob_sort_family for SPropMaxime Dénès
2020-06-23Merge PR #12552: Add a pre-hook mechanism for the `zify` tacticFrédéric Besson
2020-06-23Add a test for the strange behaviour encountered with this change.Pierre-Marie Pédrot
2020-06-22Merge PR #12434: Slight improvement in naming dependent existential variables...Gaëtan Gilbert
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 17:02:13 +0000