aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2020-08-11Merge PR #12815: [micromega] Fix bug#12790Vincent Laporte
Reviewed-by: vbgl
2020-08-11Merge PR #12814: [zify] fix for bug#12791Vincent Laporte
Reviewed-by: vbgl
2020-08-10Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)Cyril Cohen
Reviewed-by: CohenCyril Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: maximedenes Ack-by: ppedrot
2020-08-10[micromega] Fix bug#12790Frédéric Besson
zify used to generate many syntactic positivity constraints when translating a goal from nat to Z. For instance, to state that the product of 2 integers is positive. Instead, lia performs an interval analysis that is more semantic. The bug was that the interval analysis was performed after the elimination of equations. The current workaround is to perform interval analysis before and after eliminating equations. bla
2020-08-10[zify] fix for bug#12791Frédéric Besson
The elimination of let bindings is performing a convertibility check in order to deal with type aliases.
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-07-29coqdoc: Fix the “details” environmentThomas Letan
The change introduced by 41a1d66 has broken the feature prior to its initial release. We attempt to fix the issue, and add a comment to warn feature developers in order to avoid facing the same issue again.
2020-07-26Merge PR #12573: Hint Opaque/Transparent/Unfold: don't error on Opaque ↵Pierre-Marie Pédrot
Defined constants Reviewed-by: ppedrot
2020-07-24Fix coqdoc bad bulleting from incorrect space countGaëtan Gilbert
Fix #12742
2020-07-23Hint Opaque/Transparent/Unfold: don't error on opaque constantsGaëtan Gilbert
Helps with #12566
2020-07-23Merge PR #12679: Remove redundant data from VM case switch.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: silene
2020-07-23Merge PR #12698: Fixing mention of `unfold` as example of tactic taking a ↵Théo Zimmermann
qualid in tactic notations Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-07-22Merge PR #12664: Turn various anomalies into regular errors in primitive ↵Pierre-Marie Pédrot
declaration path Reviewed-by: ppedrot
2020-07-22Remove redundant data from VM case switch.Pierre-Marie Pédrot
No need to store the case_info, all the data is reconstructible from the context. Furthermore, this reconstruction is performed in a context where we already access the environment, so performance is not at stake. Hopefully this will also reduce the number of globally allocated VM values, since the switch representation now only depends on the shape of the inductive type.
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
generic printing format in anticipation of further not-only-parsing uses of the notation Reviewed-by: ppedrot
2020-07-20Merge PR #12684: Do not print constructor and inductive types as terms when ↵Gaëtan Gilbert
asked to be printed as themselves Reviewed-by: SkySkimmer
2020-07-17Add tests for the interpretation of "unfold".Hugo Herbelin
2020-07-17Merge PR #12683: Fixes #12682: printing bug with recursive notations for ↵Emilio Jesus Gallego Arias
n-ary applications used with applied references Reviewed-by: ejgallego
2020-07-17Merge PR #12631: Fix record pattern interpretation with implicit argumentsEmilio Jesus Gallego Arias
Reviewed-by: herbelin
2020-07-15Do not print global refs as terms when asked to be printed as themselves.Hugo Herbelin
This was already the case for constant, but not for constructors and inductive types. For instance, in message "The constructor @cons (in type list) is expected to ..." we don't want a @ to be printed.
2020-07-15Fix bug #12691 (an only parsing notation induces a generic printing format).Hugo Herbelin
This is to anticipate further not-only-parsing uses of the notation.
2020-07-12Fixes #12682 (recursive notation printing bug with n-ary applications).Hugo Herbelin
A special case for recursive n-ary applications was missing when the head of the application was a reference.
2020-07-11Merge PR #12650: Recordops: unify struc_typ summary record and libobject ↵Pierre-Marie Pédrot
entry struc_tuple Reviewed-by: ppedrot
2020-07-11Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/nativePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-07-10Merge PR #12666: Add test for #10890 derive vs abstractEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-10Merge PR #12537: Take into account the existing delta-resolver when starting ↵Gaëtan Gilbert
a new interactive module or module type Reviewed-by: SkySkimmer
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
This requires updating the parameter count at section end, I felt it was easier to do with rebuild_function but it could be done in discharge if needed. Incidentally fixes #12649.
2020-07-08Merge PR #12627: Fix Canonical with universe polymorphism and primitive ↵Enrico Tassi
projection Reviewed-by: ejgallego Ack-by: gares
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
Reviewed-by: ejgallego Reviewed-by: herbelin
2020-07-07Merge PR #12626: Fix Context with nonmaximplicit.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-07Fix erroneous implicits-in-term warningGaëtan Gilbert
Fix #12651
2020-07-06Merge PR #11604: Primitive persistent arraysPierre-Marie Pédrot
Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot Ack-by: proux01 Ack-by: silene
2020-07-06Correctly readback blocked CaseInvert matches in VM/nativeGaëtan Gilbert
2020-07-06Primitive persistent arraysMaxime Dénès
Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-07-05Fix Canonical with universe polymorphism and primitive projectionGaëtan Gilbert
Perhaps we should thread an evar map with the Var universes added through to cs_pattern_of_constr but that would be significantly more invasive. Fix #12528
2020-07-05Merge PR #12594: Fix ltac2 type parametersMichael Soegtrop
Reviewed-by: MSoegtropIMC Reviewed-by: gares
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
Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes
2020-07-02Fix record pattern interpretation with implicit argumentsGaëtan Gilbert
We interpret `{|proj=pat|}` as `@C _ pat` instead of `C _ pat` (where the `_` stands for the parameters). Fix #12534
2020-07-02Fix Context with nonmaximplicit.Gaëtan Gilbert
Fix #12551
2020-07-02Merge PR #12572: Correctly classify variables as being unfoldable in dnet ↵Gaëtan Gilbert
patterns. Reviewed-by: SkySkimmer Reviewed-by: maximedenes
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
Reviewed-by: SkySkimmer
2020-06-30Merge PR #11977: Generate default names for bound universes of polymorphic ↵Emilio Jesus Gallego Arias
definitions Reviewed-by: ejgallego Reviewed-by: herbelin
2020-06-29[test-suite] async-proofs off in tests with Fail TimeoutEnrico Tassi
Apparently the `Timeout` exception is raised by a signal handled, and that can happen when the running thread is a worker manager, rather than the main thread (the one that should be interrupted). Given that the point of these tests is to test *auto and not the STM, we disable async proofs forcibly.
2020-06-29Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_listPierre-Marie Pédrot
Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-23 00:59:36 +0000