aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Collapse)Author
2020-02-22Propagate implicit arguments in all notations for partial applications.Hugo Herbelin
This was done for abbreviations but not string notations. This adopts the policy proposed in #11091 to make parsing and printing consistent.
2020-02-22Fixing a bug introduced in PR #10832 (new format specific to a given notation).Hugo Herbelin
The import of the format should not be done if i<>1 in open_notation.
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
to control uniform parameters. This replaces the attribute.
2020-02-17Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)"Gaëtan Gilbert
This reverts commit bc2c1836ba4c878903288060bcb66a0ef1aaced6.
2020-02-14test for x[i] notation not breaking Ltac parsingAndres Erbsen
2020-02-14Merge PR #11584: Add #[uniform] and #[nonuniform] (for Uniform Inductive ↵Maxime Dénès
Parameters) Reviewed-by: Matafou Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2020-02-13Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)Gaëtan Gilbert
2020-02-13Arguments: removing the restriction to set an anonymous parameter implicit.Hugo Herbelin
This was already possible manually using "{ _ }" in the type of declaration. This was also possible for type classes. So, no reason to forbid in Arguments.
2020-02-11Merge PR #11235: Add syntax for non maximal implicit argumentsHugo Herbelin
Reviewed-by: herbelin Reviewed-by: jfehrle Ack-by: maximedenes
2020-02-08Remove -compat 8.9.Théo Zimmermann
Commit auto-generated by running dev/tools/update-compat.py --release. As per release doc this must be run at some point before branching (not necessarily close to the branching date).
2020-02-04Correct bug in non max local implicit argumentsSimonBoulier
+ tests in the test-suite for non max local implicit arguments
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2020-01-29Merge PR #11472: Fix #11467 ('e' was not displayed when printing decimal ↵Pierre-Marie Pédrot
notations in R) Reviewed-by: erikmd Reviewed-by: ppedrot
2020-01-28Fix #11467Pierre Roux
'e' was not displayed when printing decimal notations in R : Require Import Reals. Check (1.23e1, 32e+1, 0.1)%R. was giving < (123-1%R, 321%R, 1-1%R) instead of < (123e-1%R, 32e1%R, 1e-1%R) This was introduced in #8764 (in Coq 8.10).
2020-01-27schemes: use rigid universesGaëtan Gilbert
so for instance ~~~coq Set Printing All. Set Printing Universes. Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= . Lemma bla@{u v|u < v} : foo@{u v} -> False. Proof. induction 1. Qed. ~~~ works.
2020-01-19Merge PR #11368: Turn trailing implicit warning into an errorHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin Ack-by: maximedenes
2020-01-15Discharge inductive types without rechecking themGaëtan Gilbert
2020-01-12fix #11279. Specialize h no longer expands letins in the type of h.Pierre Courtieu
The type of h is reconstructed to look as much as the initial type of h as possible.
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Reviewed-by: ppedrot
2020-01-07Fix test-suite fo non maximal implicit argumentsSimonBoulier
2019-12-27Merge PR #11315: Ensure that a custom entry cannot be defined twice.Hugo Herbelin
Reviewed-by: herbelin Reviewed-by: maximedenes
2019-12-26Deprecate the "omega with *" syntax.Pierre-Marie Pédrot
Changes to the test-suite were backported from PR #11288.
2019-12-24[Attributes] accept #[canonical] (Let|Definition)Enrico Tassi
2019-12-24[CS] Allow a variable introduced with Let to be a canonical instanceEnrico Tassi
2019-12-23Merge PR #10760: Make rapply handle all numbers of underscoresPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-12-22Ensure that a custom entry cannot be defined twice.Pierre-Marie Pédrot
This highlights the fact that diamond inheritance of a custom entry is a tricky problem, as well as merely importing two custom entries with the same name from two different modules. The only sane way to give a semantics to that is to stick to module-scoped objects, i.e. give those entries a kernel name. In the meantime, I went for a warning when overriding entries.
2019-12-12Merge PR #11276: Fixing #10750: "Print Visibility" raises Not_found on ↵Emilio Jesus Gallego Arias
only-printing notations Ack-by: cpitclaudel Reviewed-by: ejgallego
2019-12-11Merge PR #11271: Fixing #9893. "Specialize with" would not support hyps type ↵Pierre-Marie Pédrot
containing letins. Reviewed-by: ppedrot
2019-12-10Fixing #10750 (anomaly of "Print Visibility" on only-printing notations).Hugo Herbelin
2019-12-10Merge PR #10202: Slightly more robust manual implicit argumentsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-12-10Fixing #9893 (Letins not supported in the specialized hypothesis).Pierre Courtieu
2019-12-05Unfortunate bug with "cofix with": case of a CProdN over no bindings.Hugo Herbelin
Failing on CProdN([],...) was maybe a bit too radical.
2019-12-04Manual implicit arguments: more robustness tests.Hugo Herbelin
- Warn in some places where {x:T} is not assumed to occur (e.g. in argument of an application, or of a match). - Warn when an implicit argument occurs several times with the same name. - Accept local anonymous {_:T} with explicitation possible using name `arg_k`. We obtain this by using a flag (impl_binder_index) which tells if we are in a position where implicit arguments matter and, if yes, the index of the next binder.
2019-12-03Merge PR #11113: Remove deprecated compat modifier of Notation / Infix commands.Emilio Jesus Gallego Arias
Reviewed-by: JasonGross Reviewed-by: ejgallego Reviewed-by: maximedenes
2019-12-03Merge PR #11162: [CS] support #[local] attributeMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
And simplify a lot the compatibility infrastructure following this. Update dev/tools/update-compat.py Remove much complexity. Co-authored-by: Jason Gross <jgross@mit.edu>
2019-12-02[CS] support #[local] attributeEnrico Tassi
2019-12-01Merge PR #11185: Remove deprecated Typeclasses Axioms Are Instances.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: cpitclaudel
2019-11-29Remove deprecated Typeclasses Axioms Are Instances.Théo Zimmermann
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-26Remove `rapply` tactic notation in favor of just the tacticJason Gross
This increases backwards compatibility. If desired, we can add a tactic notation to simplify the spec of `rapply` in the future if we want.
2019-11-26Make rapply handle all numbers of underscoresJason Gross
Also add a tactic notation so that it takes in uconstrs by default. Also add some basic tests for `rapply`. Also document rapply in the manual
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
We can now do `#[refine] Instance : Bla := bli.` to enter proof mode with `bli` as a starting refinement. If `bli` is enough to define the instance we still enter proof mode, keeping things nicely predictable for the stm.
2019-11-11Run update-compat script with --release option.Théo Zimmermann
This should ideally have been done before the 8.11 branching.
2019-10-30[test-suite] Test section-local mutual Fixpoint.Emilio Jesus Gallego Arias
Noticed by coverage, test code by Gäetan Gilbert. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2019-10-30Merge PR #10973: Remove dead code in save_remaining_recthmsEmilio Jesus Gallego Arias
Ack-by: JasonGross Reviewed-by: ejgallego
2019-10-27Merge PR #10827: Replace classical reals quotient axioms by functional ↵Hugo Herbelin
extensionality Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin Ack-by: maximedenes
2019-10-26Remove dead code in save_remaining_recthmsGaëtan Gilbert
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ↵Vincent Semeria
homotopy propositions and homotopy sets. Rename local variable R in test Nsatz, to avoid a name collision with the type of real numbers.
2019-10-07Call to update-compat.py.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-25 10:34:39 +0000