| Age | Commit message (Collapse) | Author |
|---|
|
similar optimization broke at some time some ssreflect code; we now
treat the easy case of a let-in to a rel - a pattern common in
pattern-matching compilation -; later on, we shall want to investigate
whether any let-in found to refer to out of scope rels or vars can be
filtered out).
|
|
|
|
|
|
propagate it. This allows C-zar to continue to work.
Don't know if it is the best way to do it.
|
|
the import of goal.ml and, afaiu, ocaml does not provide a way to
refer to a shadowed module.
|
|
|
|
|
|
status of #3278 (more precisely, it fixed a bug visible in the #3278
report, but a bug which arrived after #3278 was submitted).
|
|
|
|
|
|
- new function set_flags_for_type for setting flags when converting
types of the terms to unify
- it now sets all conversion flags, possibly restricting delta using
modulo_delta_types
- it is now used in w_unify_core_0 too
- fixing/improving documentation of options
- deprecating "Set Tactic Evars Pattern Unification"
|
|
Still to do:
- Decide between using SeveralInstancesFound or raising an error when
multiple instances exist.
- Use a proper printer for evars instead of the debugging
pr_evar_map_filter printer in pr_constraints.
|
|
types: we downcast the evar in the higher type to the lower type.
Then, we have the freedom to choose the order of instantiation
according to the instances of the evars (e.g. choosing the
instantiation for which pattern-unification is possible, if ever it is
possible in only one way - as shown by an example in contribution
Paco).
This still does not preserve compatibility because it happens that
type classes resolution is crucially dependent on the order of
presentation of the ?n=?p problems. Consider e.g. an example taken
from Containers. Both now and before e2fa65fccb9, one has this asymmetry:
Context `{Helt : OrderedType elt}.
Check forall x y r l h, @Equivalence.equiv _ _ _ x y -> In x (Node l x r h).
--> @Equivalence.equiv QArith_base.Q QArith_base.Qeq QArith_base.Q_Setoid x y
Context `{Helt : OrderedType elt}.
Check forall x y r l h, In x (Node l x r h) -> @Equivalence.equiv _ _ _ x y.
--> @Equivalence.equiv elt (@_eq elt Helt) (@OT_Equivalence elt Helt)
Then, embedding this example within a bigger one which relies on the
?n=?n' resolution order, one can get two incompatible resolution of
the same problem.
To be continued...
|
|
|
|
the non-verbose mode which I guess one wants to obey whatever
interface is used, and restoring a policy ok for coqtop - maybe would
need a change if obeying the local verbose flag is not ok for PG or
Jedit).
|
|
The occur check is done even if the flag [unsafe] is set to true. The rational is that a tactic cannot control where it takes pieces of terms from (and hence will not generally make terms which pass the occur-check), and it would be painful to ask every tactic which takes a term as an argument to do an occur check before [refine].
I reused the same error than used by unification. It gives a pretty nice error message. An alternative would be to have a dedicated error with pretty much the same error message. I'm not sure which is best, so I went for the simplest one.
The same check is done in the compatibility layer.
Fixes a reported bug which I cannot locate for some reason.
|
|
Generally, tactics build type-correct terms. A safe refine is hence a waste of time (somtimes a significant one). The safe option is kept for specific purposes such as debugging, or some weird interaction with the pretyper and universes which still seemed to hold last time I checked (used by the user-level refine tactic).
|
|
Just hoisted a definition out of a loop. Not that this part of the code is time critical at all. I just feel it's cleaner.
|
|
Instead of filtering over the goals we have just creating and running through the evar_map, fetching the evar_info (that we've just created), and marking it as unresolvable, the goals are just created unresolvable. Which is probably what I should have done from the beginning, but it had escaped my notice during my code-cleaning session.
|
|
I can't say I condone having unsafe primitives which are not used anywhere. But if they are to be there, let's make sure they don't duplicate code.
|
|
full instances.
|
|
|
|
to the first -I option.
Fortunately, with -I option, only one file can be found by occurrence
of the option, so on the contrary of -Q/-R options for v files, the
order is not file-system dependent.
|
|
|
|
|
|
types as it was before commit 710bae2a8c81a44.
There is still at least one problem with bug #3392 to solve.
|
|
possible, which is the "natural" way to orient an equation. At least
it matters for matching subterms against patterns, so that it is the
pattern variables which are substituted if ever the subterm has itself
existential variables, as in:
Goal exists x, S x = x.
eexists.
destruct (S _).
|
|
arbitrary direction as if it were an "evar = evar" problem.
|
|
Incidentally, this allows to make earlier the collapse of CUMUL to
CONV when force is true.
|
|
evar_define.
Interestingly, the added choose in evarconv.ml allows solve_evar_evar
to be observationally commutative, in the sense of not either fail or
succeed in compiling the stdlib whether problems are given in the
left-to-right or right-to-left order.
|
|
subsumed by the call to project_evar_on_evar.
|
|
normalize it afterwards.
|
|
In particular, the old hypinfo is made as a proper cache, preventing dynamic
tricks to decide whether it was rightful to refresh it.
|
|
|
|
|
|
|
|
|
|
env.
|
|
This allows to have the example in test setoid_unif.v to work again.
|
|
|
|
automatic refinement of instances, thus failing when provided with
an incomplete term instead of silently lauching the proof mode.
|
|
|
|
|
|
|
|
|
|
|
|
The function initializing proofviews were marking all evars as non-resolvables
for the proofview, while only goal evars ought to be.
|
|
|
|
|
|
When an evar was instantiated it failed to disapear from the shelf. It had the consequence of stopping Qed from happening.
Fixes test-suite/success/apply.v
|
