aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Collapse)AuthorAge
* Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\
* \ 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 ```
* | | | | Merge PR#449: make specialize smarter (bug 5370).Gravatar Maxime Dénès2017-06-01
|\ \ \ \ \
| | | | * \ Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake ↵Gravatar Maxime Dénès2017-05-31
| | | | |\ \ | | | | | | | | | | | | | | | | | | | | | (EDIT: for mutual fixpoints)
| * | | | | | Tests for new specialize feature + CHANGES.Gravatar Pierre Courtieu2017-05-31
| | | | | | |
| | * | | | | Factorizing interp_gen through a function interpreting glob_constr.Gravatar Hugo Herbelin2017-05-31
| |/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The new function is interp_glob_closure which is basically a renaming and generalization of interp_uconstr. Note a change of semantics that I could however not observe in practice. Formerly, interp_uconstr discarded ltac variables bound to names for interning, but interp_constr did not. Now, both discard them. We also export the new interp_glob_closure.
| | * | | | More precise on preventing clash between bound vars name and hidden impargs.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We want to avoid capture in "Inductive I {A} := C : forall A, I". But in "Record I {A} := { C : forall A, A }.", non recursivity ensures that no clash will occur. This fixes previous commit, with which it could possibly be merged.
| | * | | | Fixing #5233 (missing implicit arguments for recursive records).Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was failing e.g. with Inductive foo {A : Type} : Type := { Foo : foo }. Note: the test-suite was using the bug in coindprim.v.
| | * | | | Fixing a failure to interpret some local implicit arguments in Inductive.Gravatar Hugo Herbelin2017-05-31
| |/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | For instance, the following was failing to use the implicitness of n: Inductive A (P:forall m {n}, n=m -> Prop) := C : P 0 eq_refl -> A P.
* | | | | Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows a better control on the name to give to an evar and, in particular, to address the issue about naming produced by "epose proof" in one of the comment of Zimmi48 at PR #248 (see file names.v). Incidentally updating output of Show output test (evar numbers shifted).
* | | | | Few tests for e-variants of assert, set, remember.Gravatar Hugo Herbelin2017-05-30
|/ / / /
| * | | Fixing a subtle bug in tclWITHHOLES.Gravatar Hugo Herbelin2017-05-28
| | | | | | | | | | | | | | | | This fixes Théo's bug on eset.
| | | * Add equality lemmas for sig2 and sigT2Gravatar Jason Gross2017-05-28
| | | |
| | | * Add an [inversion_sigma] tacticGravatar Jason Gross2017-05-28
| |_|/ |/| | | | | | | | This tactic does better than [inversion] at sigma types.
* | | Merge PR#666: romega revisited : no more normalization trace, cleaned-up ↵Gravatar Maxime Dénès2017-05-26
|\ \ \ | | | | | | | | | | | | resolution trace
* \ \ \ Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsGravatar Maxime Dénès2017-05-25
|\ \ \ \
* \ \ \ \ Merge PR#642: Small cleanup on `close_proof` type.Gravatar Maxime Dénès2017-05-24
|\ \ \ \ \
| * | | | | [vernac] Remove `Save.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | It has been deprecated for a while in favor of `Qed`.
| | | * | | romega: discard constructor D_mono (shorter trace + fix a bug)Gravatar Pierre Letouzey2017-05-22
| | |/ / / | |/| | | | | | | | | | | | | For the bug, see new test test_romega10 in test-suite/success/ROmega0.v.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 19:24:30 +0000