aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
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
2014-09-07Test for "inversion as" naming bug.Hugo Herbelin
2014-09-07Regression test #3557Hugo Herbelin
2014-09-07Regression test for bug #2883.Hugo Herbelin
2014-09-06Fix bug #3584, elaborating pattern-matching on primitive records to theMatthieu Sozeau
use of projections.
2014-09-06Fix checker to handle projections with eta and universe polymorphism correctly.Matthieu Sozeau
2014-09-05Fix primitive projections declarations for inductive records.Matthieu Sozeau
2014-09-04Status error for bug #3459.Pierre-Marie Pédrot
2014-09-04Test for bug #3459.Pierre-Marie Pédrot
2014-09-04Fix bug #3561, correct folding of env in context[] matching.Matthieu Sozeau
2014-09-04Fix bug #3559, ensuring a canonical order of universe level quantifications whenMatthieu Sozeau
introducing constants (e.g. Top.1 is always before Top.2), compatible with the one used before introduction of hMaps in LMap/LSet.
2014-09-04Add test-suite file for Case derivation on primitive records.Matthieu Sozeau
2014-09-04Add test suite files for closed bugs.Matthieu Sozeau
2014-09-04Fix bug #3563, making syntactic matching of primitive projectionsMatthieu Sozeau
and their eta-expanded forms succeed, potentially filling parameter metavariables from the type information of the projected object.
2014-09-03Yes another remaining clearing bug with 'apply in'.Hugo Herbelin
2014-09-03Test-suite for bug #2818.Pierre-Marie Pédrot
2014-09-02Adding a test-suite for second-order matching order and indexes.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 06:40:21 +0000