aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Collapse)AuthorAge
* Merge remote-tracking branch 'github/pr/321' into v8.6Gravatar Maxime Dénès2016-10-28
|\ | | | | | | Was PR#321: Handling of section variables in hints
* \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-24
|\ \
* | | Merge branch 'v8.5' into v8.6Gravatar Hugo Herbelin2016-10-24
| | | | | | | | | | | | + a few improvements on 5f1dd4c40 (lexing of { and }).
| * | Fixing #3479 (parsing of "{" and "}" when a keyword starts with "{" or "}").Gravatar Hugo Herbelin2016-10-24
| | |
| | * sections/hints: prevent Not_found in get_type_ofGravatar Matthieu Sozeau2016-10-21
| |/ |/| | | | | | | | | | | | | due to cleared/reverted section variables. This fixes the get_type_of but requires keeping information around about the section hyps available in goals during resolution. It's optimized for the non-section case (should incur no cost there), and the case where no section variables are cleared.
* | Merge PR #300 into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
|\ \
* | | Example illustrating non-local inference of the default type of impossible ↵Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | branches (see PR #323).
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
|\ \ \ | | |/ | |/|
| * | Fixing a collision about the meta-variable ".." in recursive notations.Gravatar Hugo Herbelin2016-10-12
| | | | | | | | | | | | | | | This happens when recursive notations are used to define recursive notations.
* | | Reverting generalization and cleaning of the return clause inference in v8.6.Gravatar Hugo Herbelin2016-10-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The move to systematically trying small inversion first bumps sometimes as feared to the weakness of unification (see #5107). ---- Revert "Posssible abstractions over goal variables when inferring match return clause." This reverts commit 0658ba7b908dad946200f872f44260d0e4893a94. Revert "Trying an abstracting dependencies heuristic for the match return clause even when no type constraint is given." This reverts commit 292f365185b7acdee79f3ff7b158551c2764c548. Revert "Trying a no-inversion no-dependency heuristic for match return clause." This reverts commit 2422aeb2b59229891508f35890653a9737988c00.
* | | Clean up type classes flags and update compat file.Gravatar Maxime Dénès2016-10-05
| | |
* | | fixing bug 4609: document an option governing the generation of equalitiesGravatar Yves Bertot2016-10-03
| | | | | | | | | | | | between proofs in tactic injection, with a side-effect on inversion.
* | | More tests for tactic "subst".Gravatar Hugo Herbelin2016-10-02
| | |
| | * Move vector/list compat notations to their relevant filesGravatar Jason Gross2016-09-29
| |/ |/| | | | | | | | | | | Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations no longer modify the parser in non-compat-mode, so we can do this without breaking Ltac parsing. Also update the related test-suite files.
* | Argument : assert does fail if no arg is given (fix #4864)Gravatar Enrico Tassi2016-09-29
| |
* | Typeclass backtracking example by J. LeivantGravatar Matthieu Sozeau2016-09-28
| |
* | Merge remote-tracking branch 'github/pr/232' into v8.6Gravatar Maxime Dénès2016-09-28
|\ \ | | | | | | | | | Was PR#232: Fix the parsing of goal selectors.
* | | Posssible abstractions over goal variables when inferring match return clause.Gravatar Hugo Herbelin2016-09-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The no-inversion and maximal abstraction over dependencies now supports abstraction over goal variables rather than only on "rel" variables. In particular, it now works consistently using "intro H; refine (match H with ... end)" or "refine (fun H => match H with ... end)". By doing so, we ensure that all three strategies are tried in all situations where a return clause has to be inferred, even in the context of a "refine". See antepenultimate commit for discussion.
* | | Trying an abstracting dependencies heuristic for the match return clause ↵Gravatar Hugo Herbelin2016-09-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | even when no type constraint is given. This no-inversion and maximal abstraction over dependencies in (rel) variables heuristic was used only when a type constraint was given. By doing so, we ensure that all three strategies "inversion with dependencies as evars", "no-inversion and maximal abstraction over dependencies in (rel) variables", "no-inversion and no abstraction over dependencies" are tried in all situations where a return clause has to be inferred. See penultimate commit for discussion.
* | | Trying a no-inversion no-dependency heuristic for match return clause.Gravatar Hugo Herbelin2016-09-26
| | | | | | | | | | | | | | | | | | | | | | | | The no-inversion no-dependency heuristic was used only in the absence of type constraint. We may now use it also in the presence of a type constraint. See previous commit for discussion.
* | | Further "decide equality" tests on demand of Jason.Gravatar Hugo Herbelin2016-09-17
| | |
* | | Added a test file for contradiction.Gravatar Hugo Herbelin2016-09-15
| | |
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-14
|\ \ \ | | |/ | |/|
| * | Fixing test-suite after commit 43104a0b.Gravatar Pierre-Marie Pédrot2016-09-14
| | |
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-21
|\| |
| * | Fixing an anomaly in printing a unification error message.Gravatar Hugo Herbelin2016-08-20
| | |
* | | Merge remote-tracking branch 'origin/pr/246' into v8.6Gravatar Matthieu Sozeau2016-08-19
|\ \ \
* | | | Fixing a collision about the meta-variable ".." in recursive notations.Gravatar Hugo Herbelin2016-07-16
| | | | | | | | | | | | | | | | | | | | This happens when recursive notations are used to define recursive notations.
| * | | Add test for pi_eq_proofs.Gravatar Matthieu Sozeau2016-07-08
| | | |
* | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\ \ \ \ | |/ / / |/| / / | |/ /
* | | Fixed bug #4622.Gravatar Matthieu Sozeau2016-07-06
| | |
* | | Disallow dependent case on prim records w/o etaGravatar Matthieu Sozeau2016-07-06
| | |
* | | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2016-07-04
|\ \ \
| | * | congruence: Restrict refreshing to SetGravatar Matthieu Sozeau2016-07-04
| | | | | | | | | | | | | | | | | | | | | | | | Because refreshing Prop is not semantics-preserving, the new universe is >= Set, so cannot be minimized to Prop afterwards.
| | * | congruence/univs: properly refresh (fix #4609)Gravatar Matthieu Sozeau2016-07-04
| |/ / | | | | | | | | | | | | | | | | | | In congruence, refresh universes including the Set/Prop ones so that congruence works with cumulativity, not restricting itself to the inferred types of terms that are manipulated but allowing them to be used at more general types. This fixes bug #4609.
| | * Goal selectors now use the keyword [only].Gravatar Cyprien Mangin2016-06-30
| |/ |/| | | | | | | This fixes some parsing problems when doing things like [let n := 2 in idtac n]. See bug #4877.
* | Adding a test-suite for the only printing flag.Gravatar Pierre-Marie Pédrot2016-06-28
| |
| * Forbidding silently dropped universes instances inGravatar Matthieu Sozeau2016-06-27
| | | | | | | | | | | | internalization. Patch by PMP, test-suite fix by MS.
* | Patterns in binders: functional testsGravatar Arnaud Spiwack2016-06-27
| |
* | Test-suite fix to 1744e37 (injection in context).Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | Preserve a compatibility whether the Structural Injection flag is on or not.
* | Adding an "as" clause to specialize.Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Comments -------- - The tactic specialize conveys a somehow intuitive reasoning concept and I would support continuing maintaining it even if the design comes in my opinion with some oddities. (Note that the experience of MathComp and SSReflect also suggests that specialize is an interesting concept in itself). There are two variants to specialize: - specialize (H args) with H an hypothesis looks natural: we specialize H with extra arguments and the "as pattern" clause comes naturally as an extension of it, destructuring the result using the pattern. - specialize term with bindings makes the choice of fully applying the term filling missing expressions with bindings and to then behave as generalize. Wouldn't we like a more fine-grained approach and the result to remain in the context? In this second case, the "as" clause works as if the term were posed in the context with "pose proof".
* | Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There were three versions of injection: 1. "injection term" without "as" clause: was leaving hypotheses on the goal in reverse order 2. "injection term as ipat", first version: was introduction hypotheses using ipat in reverse order without checking that the number of ipat was the size of the injection (activated with "Unset Injection L2R Pattern Order") 3. "injection term as ipat", second version: was introduction hypotheses using ipat in left-to-right order checking that the number of ipat was the size of the injection and clearing the injecting term by default if an hypothesis (activated with "Set Injection L2R Pattern Order", default one from 8.5) There is now: 4. "injection term" without "as" clause, new version: introducing the components of the injection in the context in left-to-right order using default intro-patterns "?" and clearing the injecting term by default if an hypothesis (activated with "Set Structural Injection") The new versions 3. and 4. are the "expected" ones in the sense that they have the following good properties: - introduction in the context is in the natural left-to-right order - "injection" behaves the same with and without "as", always introducing the hypotheses in the goal what corresponds to the natural expectation as the changes I made in the proof scripts for adaptation confirm - clear the "injection" hypothesis when an hypothesis which is the natural expectation as the changes I made in the proof scripts for adaptation confirm The compatibility can be preserved by "Unset Structural Injection" or by calling "simple injection". The flag is currently off.
* | Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | simplifying and generalizing the grammar entries for injection, discriminate and simplify_eq.
* | par: like all: but in parallelGravatar Enrico Tassi2016-06-17
| | | | | | | | | | | | | | | | | | | | | | | | | | This commit documents par:, fixes its semantics so that is behaves like all:, supports (toplevel) abstract and optimizes toplevel solve. `par: solve [tac]` is equivalent to `Ltac tac1 := solve[tac]...par: tac1` but is optimized for failures: if one goal fails all are aborted immediately. `par: abstract tac` runs abstract on the generated proof terms. Nested abstract calls are not supported.
* | Tentative fix of test-suite file to avoid loopGravatar Matthieu Sozeau2016-06-16
| | | | | | | | | | Looping on jenkins only, couldn't reproduce locally. To be investigated further.
* | Cleanup and refactoringGravatar Matthieu Sozeau2016-06-16
| |
* | Revise syntax of Hint CutGravatar Matthieu Sozeau2016-06-16
| | | | | | | | | | As noticed by C. Cohen it was confusingly different from standard notation.
* | Example given at DeepSpec workshopGravatar Matthieu Sozeau2016-06-16
| |
* | Purely refactoring and code/API cleanup.Gravatar Matthieu Sozeau2016-06-16
| | | | | | | | Fix test-suite files
* | eauto: fix test-suite fileGravatar Matthieu Sozeau2016-06-16
| | | | | | | | Now that typeclasses eauto uses the new eauto.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 01:57:05 +0000