aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* Take Suggest Proof Using outside the kernel.Gravatar Gaëtan Gilbert2017-10-10
| | | | | | | | | | | | | | | | | | | Also add an output test for Suggest Proof Using. This changes the .aux output: instead of getting a key >context_used "$hyps;$suggest" where $hyps is a list of the used hypotheses and $suggest is the ;-separated suggestions (or the empty string if Suggest Proof Using is unset), there is a key >context_used "$hyps" and if Suggest Proof Using is set also a key >suggest_proof_using "$suggest" For instance instead of 112 116 context_used "B A;A B;All" we get 112 116 context_used "B A" 112 116 suggest_proof_using "A B;All"
* Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Gravatar Maxime Dénès2017-10-10
|\
* \ Merge PR #1126: [ltac] Warning for deprecated `Add Setoid` and `Add ↵Gravatar Maxime Dénès2017-10-09
|\ \ | | | | | | | | | Morphism` forms.
* \ \ Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for ↵Gravatar Maxime Dénès2017-10-09
|\ \ \ | | | | | | | | | | | | printing-ony Notations
* \ \ \ Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type ↵Gravatar Maxime Dénès2017-10-06
|\ \ \ \ | | | | | | | | | | | | | | | "_something")
* \ \ \ \ Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ↵Gravatar Maxime Dénès2017-10-06
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | inductive definition)
* \ \ \ \ \ Merge PR #1124: Extraction: reduce atomic eta-redexes (solves indirectly ↵Gravatar Maxime Dénès2017-10-06
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | BZ#4852)
| | | | | * | [ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.Gravatar Emilio Jesus Gallego Arias2017-10-05
| |_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The manual has long stated that these forms are deprecated. We add a warning for them, as indeed `Add Morphism` is an "proof evil" [*] command, and we may want to remove it in the future. We've also fixed the stdlib not to emit the warning. [*] https://ncatlab.org/nlab/show/principle+of+equivalence
| | | | | * romega: takes advantage of context variables with bodyGravatar Pierre Letouzey2017-10-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When a context variable x is of the form "x := body : Z", romega is now made aware of this body. Technically, we reify an equation x = body, and push a corresponding (eq_refl x) as argument of the final do_omega. See also the previous commit adding this same feature to omega (fixing bug 142).
| | | | | * Omega now aware of context variables with bodies (in type Z or nat) (fix bug ↵Gravatar Pierre Letouzey2017-10-05
| |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 148) For compatibility, this extra feature of omega could be disabled via Unset Omega UseLocalDefs. Caveat : for now, real let-ins inside goals or hyps aren't handled, use some "cbv zeta" reduction if you want to get rid of them. And context definitions whose types aren't Z or nat are ignored, some manual "unfold" are still mandatory if expanding these definitions will help omega.
* | | | | Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | to escape non-UTF-8 file names)
* \ \ \ \ \ Merge PR #1107: Add coqwc tests to test suiteGravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #1102: On the detection of evars which "advanced" (and a fix to ↵Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | BZ#5757)
* \ \ \ \ \ \ \ Merge PR #1101: Fixing an old proof engine bug in collecting evars with ↵Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | cleared context.
| | | | | * | | | Extraction: reduce eta-redexes whose cores are atomic (solves indirectly ↵Gravatar Pierre Letouzey2017-10-05
| |_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BZ#4852) This code simplification isn't that important, but it can trigger further simplifications elsewhere, see for instance BZ#4852. NB: normally, the extraction favors eta-expanded forms, since that's the usual way to avoid issues about '_a type variables that cannot be generalized. But the atomic eta-reductions done here shouldn't be problematic (no applications put outside of functions).
| | | | | | * | Fixing BZ#5769 (variable of type "_something" was named after invalid "_").Gravatar Hugo Herbelin2017-10-05
| | | | | | | |
| | | | | * | | Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).Gravatar Hugo Herbelin2017-10-05
| | | | | |/ /
* | | | | | | Merge PR #1006: fix: ssrmatching and primitive projectionsGravatar Maxime Dénès2017-10-04
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #1078: Report missing arguments in error messageGravatar Maxime Dénès2017-10-04
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial).Gravatar Maxime Dénès2017-10-04
|\ \ \ \ \ \ \ \ \
| | | | | | * | | | add coqwc testsGravatar Paul Steckler2017-10-03
| | | | | | | |/ / | | | | | | |/| |
* | | | | | | | | Merge PR #1012: Make a test for coq_makefile portable.Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \
* | | | | | | | | | [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
| |_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why.
| | | | | | * | | Moving setting of "cleared" evar flag directly in Evd.restrict.Gravatar Hugo Herbelin2017-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In particular, this fixes #5757 which used restrict_evar to refine the information on the source of an evar, and which should have set the "cleared" flag. Also renaming flag "restricted" since it is not only about "clear". I guess this is what we want in general, but I did not survey all uses of restrict_evar so, maybe, this should be refined further.
| | | | | | * | | Fixing an old bug in collecting evars with cleared context.Gravatar Hugo Herbelin2017-09-27
| |_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The function Proofview.undefined was collecting twice the evars that had advanced. Consequently, the functions Proofview.unshelve and Proofview.with_shelf were possibly doing the same.
| | | | | * | | Fixing an old bug in collecting evars with cleared context.Gravatar Hugo Herbelin2017-09-27
| |_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The function Proofview.undefined was collecting twice the evars that had advanced. Consequently, the functions Proofview.unshelve and Proofview.with_shelf were possibly doing the same.
* | | | | | | Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\ \ \ \ \ \ \
| | | | | | | * BZ#5739, Allow level for leftmost nonterminal for printing-ony NotationsGravatar Paul Steckler2017-09-25
| | | | | | | |
* | | | | | | | Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ↵Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | inductive types)
* \ \ \ \ \ \ \ \ Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ↵Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | let-ins and non-recursively uniform parameters
* \ \ \ \ \ \ \ \ \ Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in ↵Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 4e70791).
* \ \ \ \ \ \ \ \ \ \ Merge PR #1060: An optimization of tactic constructorGravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \ \
| | | | * | | | | | | | Fixing #5755 (discharging of inductive types not correct with let-ins).Gravatar Hugo Herbelin2017-09-23
| |_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The number of effective parameters was used where the number of declarations in the signature of parameters should have been used.
| | * | | | | | | | | Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).Gravatar Hugo Herbelin2017-09-23
| | | |_|_|_|_|_|_|/ | | |/| | | | | | |
| | | * | | | | | | Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Gravatar Hugo Herbelin2017-09-23
| |_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The bug was caused by an inconsistency in different part of the code for deciding where cutting the context in between recursively uniform parameters and non-recursively uniform ones when let-ins were in the middle. We fix it by using uniformly "context_chop".
| | | | * | | | | Make a test for coq_makefile portable.Gravatar Pierre-Marie Pédrot2017-09-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The validity of this test depended on Makefile issueing warnings in English. We simply force the global language of the shell to be C.
| | | | | | * | | Report missing arguments in error messageGravatar Tej Chajed2017-09-21
| | | |_|_|/ / / | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Augment the "Illegal tactic application" error message with the number of extra arguments passed. Fixes BZ#5753.
* | / | | | | | A possible fix to BZ#5750 (ability to print context of ltac subterm match).Gravatar Hugo Herbelin2017-09-21
| |/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | The main fix is to use is_ident_soft. The rest of the commit is to provide something a bit more appealing than "?M-1".
| | | | | * | ssr: fix canonical strucut key comparison with primproj onGravatar Enrico Tassi2017-09-20
| | | | |/ / | | | |/| |
| * | / | | An optimization of tactic constructor.Gravatar Hugo Herbelin2017-09-19
|/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As was questioned on Stack Overflow and discussed on Gitter, reduction of the conclusion of the goal was done up to n+1 times for a failing call to "constructor" on an inductive type of n constructors. We do it at most once. Reworking the layout of the code at the same time.
| | | * / Fixing bug #5741 (anomaly in info_trivial).Gravatar Hugo Herbelin2017-09-19
| |_|/ / |/| | | | | | | | | | | The bug was introduced in 1559f73.
* | | | Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).Gravatar Maxime Dénès2017-09-19
|\ \ \ \
| | * | | Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
| | | | | | | | | | | | | | | | | | | | | | | | | We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it.
| | * | | test-suite: polymorphismGravatar Matthieu Sozeau2017-09-19
| | | | |
| | * | | Allow declaring universe binders with no constraints with @{|}Gravatar Gaëtan Gilbert2017-09-19
| | | | |
| | * | | Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
| | |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j | }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions.
* | | | Merge PR #920: kernel: bugfix in filter_stack_domain.Gravatar Maxime Dénès2017-09-19
|\ \ \ \ | |_|/ / |/| | |
| * | | Add test-suite script by Cyprien ManginGravatar Matthieu Sozeau2017-09-18
| | | |
* | | | Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" ↵Gravatar Maxime Dénès2017-09-15
|\ \ \ \ | | | | | | | | | | | | | | | Inductive-keyworded record failing even on non-dependent goal)
* \ \ \ \ Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" ↵Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | work better on them
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 15:11:37 +0000