aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2014-09-27Fix bug #3664 by refolding projections that don't reduce in cbn.Matthieu Sozeau
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-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-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-25Fix incorrect assert false in detyping.Matthieu Sozeau
2014-09-24Rename eq_constr functions in Evd to not break backward compatibilityMatthieu Sozeau
with existing ML code.
2014-09-24Return a Prop not an arbitrary Type, and correct a typo.Matthieu Sozeau
2014-09-24Make eq_pattern_test/eq_test work up to the equivalence of primitiveMatthieu Sozeau
projections with their eta-expanded constant form.
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-19Fixes in Ltac pattern-matching on primitive projectionsMatthieu Sozeau
and pretyping which was not contracting the eta-expanded forms in presence of coercions.
2014-09-19Use smart mapping in map_constr_with_binders_left_to_right.Matthieu Sozeau
2014-09-19Fixing #3641 (loop in e_contextually, introduced in r16525).Hugo Herbelin
2014-09-19Revert change of e_contextually as it needlessly expands all primitiveMatthieu Sozeau
projections in the term.
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-18Do not try to match on a subterm that is not closed in find_subterm.Matthieu Sozeau
2014-09-18For type classes, tell that VarInstance's behave like GoalEvar (avoid a loop ↵Hugo Herbelin
in Class_tactics).
2014-09-18Reductionops: (Co)Fixpoints are always refolded during iotaPierre Boutillier
2014-09-17Be more conservative and keep the use of eq_constr in pretyping/ functions.Matthieu Sozeau
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-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-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-15Fix: when interpreting a identifier in pretying, use the Ltac identifier ↵Arnaud Spiwack
substitution at the right place. I used to change [id] to its interpretation before calling [pretype_id]. But it's incorrect: we need to use the Ltac interpretation only when looking up the rel context (where it has been interpreted previously). It would not be to use the interpreted identifier to look up the named context or the Ltac context.
2014-09-15Fix a bug in the naming of binders.Arnaud Spiwack
The ident closure was not propagated when pretying a [uconstr] coming from a [uconstr] closure. This bug had never been reported, as far as I'm aware.
2014-09-15Fix bug #3610, allowing betaiotadelta reduction while unifying types ofMatthieu Sozeau
records in unification.ml.
2014-09-15Fix bug #3621, using fold_left2 on arrays of the same size only.Matthieu Sozeau
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-13Using "Evd.restrict" in tactic clear so as to keep evar names.Hugo Herbelin
2014-09-13Exporting apply_subfilter from Evd.ml.Hugo Herbelin
2014-09-13Fixing synchronization of evar names table when merging evar_map.Hugo Herbelin
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-09-13Checking typability of evar instances. Using ";" to separate bindingsHugo Herbelin
in instances.
2014-09-12An old typo which was preventing example #3537 to work the same as itHugo Herbelin
was working in 8.4.
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12Parsing evar instances.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions.
2014-09-11Add a flag for restricting resolution of typeclasses toMatthieu Sozeau
matching (i.e. no instanciation of the goal evars). Classes defined when [Set Typeclasses Strict Resolution] is on use the restricted resolution for all their instances (except for Hint Extern's).
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-10A step towards better differentiating when w_unify is used for subtermHugo Herbelin
selection (rewrite, destruct/induction, set or apply on scheme), for unification (apply on not a scheme, auto), the latter being separated into primary unification and unification for merging instances. No change of semantics from within Coq, if I did not mistake (but a function like secondOrderAbstraction does not set flags by itself anymore).
2014-09-10Fix generation of inductive elimination principle for primitive records.Matthieu Sozeau
Let r.(p) be a strict subterm of r during the guardness check.
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-08Parsing of Type@{max(i,j)}.Matthieu Sozeau
2014-09-08Fix bug #3589, unification looping due to incorrect use of stack with ↵Matthieu Sozeau
primitive projections.
2014-09-06Fix bug #3584, elaborating pattern-matching on primitive records to theMatthieu Sozeau
use of projections.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 00:17:43 +0000