aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Collapse)AuthorAge
* Moving bug numbers to BZ# format in the test-suite.Gravatar Théo Zimmermann2017-10-19
| | | | | Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers.
* Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Gravatar Maxime Dénès2017-10-10
|\
* | [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).
* Merge PR #1101: Fixing an old proof engine bug in collecting evars with ↵Gravatar Maxime Dénès2017-10-05
|\ | | | | | | cleared context.
* | [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.
| * 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
|\
* | 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".
| * 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 #986: Ensuring all .v files end with a newline to make "sed -i" ↵Gravatar Maxime Dénès2017-09-15
|\ \ | | | | | | | | | work better on them
* | | Fixing little inaccuracy in coercions to ident or name.Gravatar Hugo Herbelin2017-09-12
| | | | | | | | | | | | For instance, we don't want "id@{u}" to be coerced to id, or "?[n]" to "_".
* | | Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\ \ \
| | * | Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
| |/ / |/| |
* | | Merge PR #864: Some cleanups after cumulativity for inductive typesGravatar Maxime Dénès2017-08-16
|\ \ \
| * | | Change the option for cumulativityGravatar Amin Timany2017-07-31
| | | |
| * | | Add Jason's example of fun-ext with cumulativityGravatar Amin Timany2017-07-31
| | | |
| * | | Add test for NonCumulative inductivesGravatar Amin Timany2017-07-31
| | | |
| * | | Issue error on monomorphic cumulative inductivesGravatar Amin Timany2017-07-31
| | |/ | |/|
* | | test-suite: more use of the new command Extraction TestCompileGravatar Pierre Letouzey2017-07-27
| | |
* | | test-suite/success/extraction.v : add some Extraction TestCompileGravatar Pierre Letouzey2017-07-26
|/ /
* | Remove non-terminating Timeout tests from Hints.v.Gravatar Maxime Dénès2017-07-20
| |
* | Getting rid of abstraction breaking code in tclABSTRACT.Gravatar Pierre-Marie Pédrot2017-07-14
| | | | | | | | | | | | | | | | | | | | | | This is probably the hardest case of them all, because tclABSTRACT fundamentally relies on the names of universes from the constant instance being the same as the one in the current goal. Adding to that the fact that the kernel is doing strange things when provided with a polymorphic definition with body universe constraints, it turns out to be a hellish nightmare to handle properly. At some point we need to clarifiy this in the kernel as well, although we leave it for some other patch.
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| |
| * Reorganizing functions to find the relative position of an hypothesis.Gravatar Hugo Herbelin2017-06-25
| | | | | | | | | | Also fixing a bug of get_next_hyp_position when the hypothesis is the oldest of the context (see test in ltac.v).
| * Moving "assert" (internally "Cut") to the new proof engine.Gravatar Hugo Herbelin2017-06-25
| | | | | | | | | | It allows in particular to have "Info" on tactic "assert" and derivatives not to give an "<unknown>".
* | Add test-suite file for funind, extraction with compat 8.6Gravatar Jason Gross2017-06-22
|/
* Merge PR#807: romega: fix a slowdownGravatar Maxime Dénès2017-06-20
|\
| * romega: avoid potential slowdown when changing concl by reified versionGravatar Pierre Letouzey2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | On some benchmarks provided by Chantal Keller a long time ago, romega was abnormally slow compared to omega (or lia). It turned out that the change of concl by reified version was triggering unnecessary unfolds of Z.add, instead of unfolding ReflOmegaCore.Z_as_Int.plus into Z.add. This is now fixed by the various Parameter Inline : no more indirections, Z_as_Int.plus is directly Z.add. Also use Tactics.convert_concl_no_check for this "change", as recommended by PMP.
* | Fix a bug in cumulativityGravatar Amin Timany2017-06-16
| |
* | Move (part of) tests from checker to successGravatar Amin Timany2017-06-16
| | | | | | | | | | | | Due to some unknown problem coqchk fails on some inductive types when it is compiled with ocaml4.02.3+32bit and camlp5-4.16 which is the case for Travis tests.
* | Disable debug printingGravatar Amin Timany2017-06-16
| | | | | | | | Fix a mistake in record declaration
* | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
| |
* | Fix bugsGravatar Amin Timany2017-06-16
|/
* Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\
* \ Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \
* | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
| | * Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| |/ |/|
* | Merge PR#498: Bignums as a separate opam packageGravatar Maxime Dénès2017-06-14
|\ \
* \ \ Merge PR#385: Equality of sigma typesGravatar Maxime Dénès2017-06-13
|\ \ \
| | * | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
| |/ / |/| | | | | | | | | | | | | | See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude.
| | * A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
| |/ |/| | | | | | | | | | | | | | | Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let".
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \
* \ \ Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a ↵Gravatar Maxime Dénès2017-06-06
|\ \ \ | | | | | | | | | | | | short econstr-cleaning of record.ml
* \ \ \ Merge PR#600: Some factorizations of ltac interpretation functions between ↵Gravatar Maxime Dénès2017-06-06
|\ \ \ \ | | | | | | | | | | | | | | | ssreflect and coq code
* | | | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 02:42:18 +0000