aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2014-09-27Fix semantics of matching with folded/unfolded projections to definitelyMatthieu Sozeau
avoid looping and be compatible with unfold.
2014-09-27Fix bug #3672, application of primitive projections as coercions.Matthieu Sozeau
2014-09-27Fix bug 3662 by actually reducing primitive projections in cbv/compute.Matthieu Sozeau
2014-09-27Bug fixed.Matthieu Sozeau
2014-09-27Make pattern_of_constr typed so that we can infer the proper patternsMatthieu Sozeau
for primitive projections, fixing bug #3661. Also fix expand_projection so that it does enough reduction to find the inductive type of its argument.
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections.
2014-09-27Adapting to naming of evars.Hugo Herbelin
2014-09-26Fix canonical structure resolution which was launched on the results ofMatthieu Sozeau
eta-expansion, creating a loop. This is now deactivated. Fixes bugs #3665 and #3667.
2014-09-26Add a bunch of reproduction files for bugs.Xavier Clerc
2014-09-26Add missing "Fail" to bug cases.Xavier Clerc
2014-09-26Bug #3566 is fixed.Xavier Clerc
2014-09-26Adding a test for bug #3653.Pierre-Marie Pédrot
2014-09-26Test cases for closed bugs.Xavier Clerc
2014-09-25Add several reproduction files for bugs.Xavier Clerc
2014-09-24Update test-suite files.Matthieu Sozeau
2014-09-23Fix bug #3656.Matthieu Sozeau
Maintain the user-level view of primitive projections, disallow manual unfolding and do not let hnf give the eta-expanded form.
2014-09-19Move the specific map_constr_with_binders_left_to_rightMatthieu Sozeau
for e_contextually where it is used. Bug #3648 is fixed.
2014-09-19Fixing #3641 (loop in e_contextually, introduced in r16525).Hugo Herbelin
2014-09-18Fix constrMatching as well as change/e_contextually to allowMatthieu Sozeau
matching partial applications of primitive projections. Fixes bug #3637.
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
Add a flag to indicate if we're in the toplevel or debuggger to not try to retype terms in the wrong environment (and making find_rectype, get_type_of untraceable). This fixes bug #3638 along with the previous commit.
2014-09-18Reductionops: (Co)Fixpoints are always refolded during iotaPierre Boutillier
2014-09-17Fix bug #3593, making constr_eq and progress work up toMatthieu Sozeau
equality of universes, along with a few other functions in evd.
2014-09-17Fix bug #3633 properly, by delaying the interpetation of constrs inMatthieu Sozeau
apply f, g,... so that apply f, g. succeeds when apply f; apply g does. It just mimicks the behavior of rewrite foo bar.
2014-09-17Revert "While resolving typeclass evars in clenv, touch only the ones that ↵Matthieu Sozeau
appear in the" This reverts commit 9de1edd730eeb3cada742a27a36bc70178eda6d8. Not the right way to do it. The evd shouldn't contain unrelated evars in the first place.
2014-09-17While resolving typeclass evars in clenv, touch only the ones that appear in theMatthieu Sozeau
clenv's value and type, ensuring we don't try to solve unrelated goals (fixes bug#3633).
2014-09-17Update test-suite files after last commit. Add a file for rewrite_stratMatthieu Sozeau
examples.
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
contortions in internalization/externalization. It uses a fully typed version of detyping, requiring the environment, to move from primitive projection applications to regular applications of the eta-expanded version. The kernel is unchanged, and only constrMatching needs compatibility code now.
2014-09-16Undo prints only if coqtop || emacsEnrico Tassi
2014-09-16fix test-suite/success/decl_mode.vEnrico Tassi
2014-09-15Add a "Hint Mode ref (+ | -)*" hint for setting a global modeMatthieu Sozeau
of resulution for goals whose head is "ref". + means the argument is an input and shouldn't contain an evar, otherwise resolution fails. This generalizes the Typeclasses Strict Resolution option which prevents resolution to fire on underconstrained typeclass constraints, now the criterion can be applied to specific parameters. Also cleanup auto/eauto code, uncovering a potential backwards compatibility issue: in cases the goal contains existentials, we never use the discrimination net in auto/eauto. We should try to set this on once the contribs are stabilized (the stdlib goes through when the dnet is used in these cases).
2014-09-15Adapting ltac output test to new interpretation of binders.Hugo Herbelin
2014-09-15Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.Hugo Herbelin
2014-09-15Fixing line break in test for #3559.Hugo Herbelin
2014-09-15Avoid backtracking in typeclass search if a solution for a closedMatthieu Sozeau
non-dependent or propositional constraint has already been found (same behavior as before previous patch).
2014-09-15Rework typeclass resolution and control of backtracking.Matthieu Sozeau
Add a global option to check for multiple solutions and fail in that case. Add another flag to declare classes as having unique instances (not checked but assumed correct, avoiding some backtracking).
2014-09-13Fixing injection bug #3616 on sigma-types.Hugo Herbelin
2014-09-12While we don't have a clean alternative to Clenvtac, add a primitiveMatthieu Sozeau
for tclEVARS which might solve existing goals.
2014-09-12An old typo which was preventing example #3537 to work the same as itHugo Herbelin
was working in 8.4.
2014-09-11Fix test-suite files, and move some opened to closed.Matthieu Sozeau
2014-09-11Other bugs with "inversion as" (collision between user-provided names and ↵Hugo Herbelin
generated equation names).
2014-09-11Fix bug #3594: eta for constructors and functions at the same time whichMatthieu Sozeau
was failing in this case due to the wrong postponment of an unsolvable ?X = RigidContext[?X] problem.
2014-09-11Fix bug #3596, wrong treatment of projections in compute_constelim_direct.Matthieu Sozeau
2014-09-11Fix bug #3505.Matthieu Sozeau
When w_unifying primitive projection applications, force the unification of types of the projected records to recover instances for the parameters (evarconv does this automatically by unifying evar instances with their expected type).
2014-09-10Parsing and printing of primitive projections, fix buggy behavior whenMatthieu Sozeau
implicits do not allow to parse as an application and cleanup code.
2014-09-10Fixing inversion after having fixed intros_replacingHugo Herbelin
in69665dd2480d364162933972de7ffa955eccab4d. There are still situations when "as" is not given where equations coming from injection are not yet removed, making invalid the computation of dependencies, what prevents an hypothesis to be cleared and replaced.
2014-09-10Example for apply and evars.Hugo Herbelin
2014-09-09- Fix printing and parsing of primitive projections, including the SetMatthieu Sozeau
Printing All cases (bug #3597). - Fix Ltac matching with primitive projections (bug #3598). - Spotted a problem with printing of constants with maximally implicit arguments due to strange "compatibility" interpretation of Arguments [X] as Arguments {X} but didn't fix it entirely yet (might cause incompatibilities).
2014-09-08Fixing TestRefine test-suite file.Pierre-Marie Pédrot
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-09-08Parsing of Type@{max(i,j)}.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-12 01:37:50 +0000