aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
| | | | | | | | | | (the action is "clear"). Added subst_intropattern which was missing since the introduction of ApplyOn intro patterns. Still to do: make "intros _ ?id" working without interferences when "id" is precisely the internal name used for hypotheses to discard.
* Restoring non-uniform delta on local and global constants in 2nd orderGravatar Hugo Herbelin2014-09-29
| | | | | unification for apply (compatibility reason). Waiting for another way to provide a more uniform scheme by default (keyed unification?).
* Adding a test for bug #2428.Gravatar Pierre-Marie Pédrot2014-09-29
|
* Bug fixed.Gravatar Matthieu Sozeau2014-09-29
|
* Fix test-suite filesGravatar Matthieu Sozeau2014-09-29
| | | | | 3566 gave a legitimate error, keyedrewrite was not setting keyed unification on.
* In evarconv and unification, expand folded primitive projections toGravatar Matthieu Sozeau2014-09-29
| | | | | | | | | | their eta-expanded forms which can then unfold back to the unfolded primitive projection form. This removes all special code that was necessary to handle primitive projections before, while keeping compatibility. Also fix cbn which was not refolding primitive projections correctly in all cases. Update some test-suite files accordingly.
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | (but deactivated still). Set Keyed Unification to activate the option, which changes subterm selection to _always_ use full conversion _after_ finding a subterm whose head/key matches the key of the term we're looking for. This applies to rewrite and higher-order unification in apply/elim/destruct. Most proof scripts already abide by these semantics. For those that don't, it's usually only a matter of using: Declare Equivalent Keys f g. This make keyed unification consider f and g to match as keys. This takes care of most cases of abbreviations: typically Def foo := bar and rewriting with a bar-headed lhs in a goal mentioning foo works once they're set equivalent. For canonical structures, these hints should be automatically declared. For non-global-reference headed terms, the key is the constructor name (Sort, Prod...). Evars and metas are no keys. INCOMPATIBILITIES: In FMapFullAVL, a Function definition doesn't go through with keyed unification on.
* First version of keyed subterm selection in unification.Gravatar Matthieu Sozeau2014-09-27
|
* Fix test-suite file.Gravatar Matthieu Sozeau2014-09-27
|
* Fix bug #3664 by refolding projections that don't reduce in cbn.Gravatar Matthieu Sozeau2014-09-27
|
* Fix semantics of matching with folded/unfolded projections to definitelyGravatar Matthieu Sozeau2014-09-27
| | | | avoid looping and be compatible with unfold.
* Fix bug #3672, application of primitive projections as coercions.Gravatar Matthieu Sozeau2014-09-27
|
* Fix bug 3662 by actually reducing primitive projections in cbv/compute.Gravatar Matthieu Sozeau2014-09-27
|
* Bug fixed.Gravatar Matthieu Sozeau2014-09-27
|
* Make pattern_of_constr typed so that we can infer the proper patternsGravatar Matthieu Sozeau2014-09-27
| | | | | | for primitive projections, fixing bug #3661. Also fix expand_projection so that it does enough reduction to find the inductive type of its argument.
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
| | | | | | | | 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.
* Adapting to naming of evars.Gravatar Hugo Herbelin2014-09-27
|
* Fix canonical structure resolution which was launched on the results ofGravatar Matthieu Sozeau2014-09-26
| | | | eta-expansion, creating a loop. This is now deactivated. Fixes bugs #3665 and #3667.
* Add a bunch of reproduction files for bugs.Gravatar Xavier Clerc2014-09-26
|
* Add missing "Fail" to bug cases.Gravatar Xavier Clerc2014-09-26
|
* Bug #3566 is fixed.Gravatar Xavier Clerc2014-09-26
|
* Adding a test for bug #3653.Gravatar Pierre-Marie Pédrot2014-09-26
|
* Test cases for closed bugs.Gravatar Xavier Clerc2014-09-26
|
* Add several reproduction files for bugs.Gravatar Xavier Clerc2014-09-25
|
* Update test-suite files.Gravatar Matthieu Sozeau2014-09-24
|
* Fix bug #3656.Gravatar Matthieu Sozeau2014-09-23
| | | | | | Maintain the user-level view of primitive projections, disallow manual unfolding and do not let hnf give the eta-expanded form.
* Move the specific map_constr_with_binders_left_to_rightGravatar Matthieu Sozeau2014-09-19
| | | | for e_contextually where it is used. Bug #3648 is fixed.
* Fixing #3641 (loop in e_contextually, introduced in r16525).Gravatar Hugo Herbelin2014-09-19
|
* Fix constrMatching as well as change/e_contextually to allowGravatar Matthieu Sozeau2014-09-18
| | | | matching partial applications of primitive projections. Fixes bug #3637.
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
| | | | | | | 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.
* Reductionops: (Co)Fixpoints are always refolded during iotaGravatar Pierre Boutillier2014-09-18
|
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
| | | | equality of universes, along with a few other functions in evd.
* Fix bug #3633 properly, by delaying the interpetation of constrs inGravatar Matthieu Sozeau2014-09-17
| | | | | apply f, g,... so that apply f, g. succeeds when apply f; apply g does. It just mimicks the behavior of rewrite foo bar.
* Revert "While resolving typeclass evars in clenv, touch only the ones that ↵Gravatar Matthieu Sozeau2014-09-17
| | | | | | | | 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.
* While resolving typeclass evars in clenv, touch only the ones that appear in theGravatar Matthieu Sozeau2014-09-17
| | | | | clenv's value and type, ensuring we don't try to solve unrelated goals (fixes bug#3633).
* Update test-suite files after last commit. Add a file for rewrite_stratGravatar Matthieu Sozeau2014-09-17
| | | | examples.
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
| | | | | | | | 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.
* Undo prints only if coqtop || emacsGravatar Enrico Tassi2014-09-16
|
* fix test-suite/success/decl_mode.vGravatar Enrico Tassi2014-09-16
|
* Add a "Hint Mode ref (+ | -)*" hint for setting a global modeGravatar Matthieu Sozeau2014-09-15
| | | | | | | | | | | | | 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).
* Adapting ltac output test to new interpretation of binders.Gravatar Hugo Herbelin2014-09-15
|
* Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.Gravatar Hugo Herbelin2014-09-15
|
* Fixing line break in test for #3559.Gravatar Hugo Herbelin2014-09-15
|
* Avoid backtracking in typeclass search if a solution for a closedGravatar Matthieu Sozeau2014-09-15
| | | | | non-dependent or propositional constraint has already been found (same behavior as before previous patch).
* Rework typeclass resolution and control of backtracking.Gravatar Matthieu Sozeau2014-09-15
| | | | | | | 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).
* Fixing injection bug #3616 on sigma-types.Gravatar Hugo Herbelin2014-09-13
|
* While we don't have a clean alternative to Clenvtac, add a primitiveGravatar Matthieu Sozeau2014-09-12
| | | | for tclEVARS which might solve existing goals.
* An old typo which was preventing example #3537 to work the same as itGravatar Hugo Herbelin2014-09-12
| | | | was working in 8.4.
* Fix test-suite files, and move some opened to closed.Gravatar Matthieu Sozeau2014-09-11
|
* Other bugs with "inversion as" (collision between user-provided names and ↵Gravatar Hugo Herbelin2014-09-11
| | | | generated equation names).