| Age | Commit message (Collapse) | Author |
|---|
|
|
|
early call the standard resolution function which e.g. does
restriction and maybe solve the problem if pattern-like, instead of
postponing the problem.
|
|
|
|
don't print bindings of the form "x:=x" unless there is also a binding
"x':=x". Otherwise said, if a variable occurs several time, the
binding where it occurs under the form "x:=x" is printed anyway. This
should help to understand where the instance is non trivial while
still not obfuscating display in goals with very long list of
uninteresting trivial instances.
|
|
|
|
Proofs of C t1..tn+1 = C t1..tn+1, even when the terms were
syntactically the same, were built by composition of a proof of C
t1..tn = C t1..tn with a proof of reflexivity of tn+1. The latter was
reduced to showing C t1..tn = C u1..un for C u1..un the canonical
representant of C t1..tn in its congruence class. But if some pair
ti=ui was derivable by injectivity of the constructor C, it might go
back to find a proof of C t1..tn+1 = C t1..tn+1 again, while a simple
reflexivity proof was enough here.
Not sure that the fix prevents any further loop in this part of the
code though.
|
|
|
|
Commit 3e972b3ff8e532be233f70567c87512324c99b4e renamed coq.el,
coq-db.el, coq-syntax.el to gallina.el, gallina-db.el,
gallina-syntax.el without fixing up any of the references. Commit
30b58d43e48569afb50a35d3915ec7d453a61f5d only fixed up some of them.
Here are some more (hopefully all of them).
Signed-off-by: Anders Kaseorg <andersk@mit.edu>
|
|
(continuation of 3087e0012eb12833a79b and 1f05decaea97f1dc).
It may be the case that the new expression lives in a higher sorts and
the context where it is substituted in supports it. So, it is too
strong to expect that, when the substituted objects are types, the
sort of the new one is smaller than the sort of the original
one. Consider e.g.
Goal @eq Type nat nat.
change nat with (@id Type nat).
which is a correct replacement, even if (id Type nat) is in a higher sort.
Introducing typing in "contextually" would be a big change for a
little numbers of uses, so we instead (hackily) recheck the whole term
(even though typing with evars uses evar_conv which accept to unify
Type with Set, leading to wrongly accept "Goal @eq Set nat nat.
change nat with (@id Type nat).". Evar conv is however rejecting
Prop=Type.)
|
|
(Maybe one of the source of inefficiency introduced on Oct 9 - see e.g. CoLoR.)
|
|
(More thinking needed)
|
|
Makes the monad more flexible as it will be easier to add new components to the concrete state of the tactic monad.
The Proofview module is also organised in a more abstract way with dedicated submodules to access various parts of the state or writer.
|
|
|
|
|
|
|
|
Changes in the implementation details had unwittingly changed the order in which Grab Existential Variables displayed the goals.
|
|
|
|
Uses the new architecture which allows to keep track of all new evars. The [future_goals] are flushed at the end of the tactics, the [principal_future_goal] is ignored.
|
|
In my first attempt I just dropped all future goals before starting a refinement. This was done for simplicity but is incorrect in general. In this version the future goals which are not introduced by the particular instance of refine are kept for future use.
|
|
Now [Goal] only contains a few helpers.
|
|
|
|
The rest will take more work.
|
|
We are left with the compatibility layer and a handful of primitives which require some thought to move.
|
|
First step in removing the [Goal] module whose code is now essentially legacy.
Removes the cache attached to a goal, which was used to avoid unnecessary [nf_evar]. May have a performance cost, which is to be fixed later.
|
|
|
|
|
|
Now, usual function from Evarutil are used to define evars instead of the variants from Proofview.Refine.
The [update] primitive which tried to patch the difference between pretyping functions and the refine primitive is now replaced by the identity function.
|
|
See previous commit for more discussion.
Changed the name from "main" to "principal" because I find "main" overused, and because the name was only introduced yesterday anyway.
|
|
That way, everything in the code of pretying is made "refine"-aware. Making the abstraction stonger and integration of pretyping with interactive proof more direct.
It might create goals in a slightly different goal order in the (user level) refine tactic. Because now, the [update] primitive which used to infer an order from an [evar_map] now has the order fixed by the successive declaration with [Evarutil.new_evar] (and similar). It probably coincides, though.
Following a suggestion by Hugo.
|
|
|
|
|
|
[refine].
This makes [new_evar] closer to be a mere wrapper around [Evarutil.new_evars]. Will allow restructuring of the refinement interface.
|
|
|
|
parameters.
|
|
|
|
projections in cbv when delta _and_ beta flags are set. Add test-suite
file for bug 3700 too.
|
|
primitive record.
|
|
|
|
Fix typeclass resolution which was considering as subgoals
of a tactic application unrelated pre-existing undefined evars.
|
|
|
|
|
|
|
|
|
|
now fails with Error: Already an existential evar of name Main
|
|
|
|
forms in evarconv and unification, as well as fallback to first-order
unification when eta for constructors fail. Update test-suite file
3484 to test for the FO case in evarconv as well.
|
|
of the record binder for Class C's projections.
|
|
folded primitive projections in applicative stacks in rhs as named, hence
prefering to unfold the lhs in these cases.
|
|
required, i.e. in first-order unification cases where the head of the
other side is a hole or the eta-expanded constant.
|
|
make printing exponentially slower. We would have to expand all projections
at once before detyping to make this linear.
|
