| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
defined and the file providing the primitives.
The datatypes are defined in [Proofview_monad], previous [Proofview_monad] is now called [Logic_monad] since it is more generic since the refactoring.
|
|
ret -> return, bind -> (>>=), etc… So that monads expose a [Monad.S] signature. Also Proofview now exposes the [Monad.S] signature directly rather than in a [Monad.S] subdirectory.
|
|
[on_advance] gave almost no gain in readability, while costing a closure.
|
|
|
|
dispatch.
Leads to clearer an more efficient code.
|
|
|
|
For optimisation purposes.
|
|
|
|
|
|
It is, after all, a generic function about lists.
|
|
combinators.
|
|
|
|
The monadic bind can be costly, so sparing a few can be worth it. Therefore I unrolled the last element of the recursions. I took the opportunity to do some loop unrolling, which is probably more useful for map combinators than for fold.
|
|
|
|
|
|
|
|
|
|
The Unsafe module is for unsafe tactics which cannot be done without anytime soon. Whereas V82 indicates a function which we want to get rid of and that shouldn't be used in a new function.
|
|
|
|
|
|
|
|
That is [Tactics.New.refine]. Replaced it with a wrapper around the primitive refine [Proofview.Refine.refine], but with extra reductions on the resulting goals.
There was two used of this refine: one in the declarative mode, and one in type classes. The porting of the latter is likely to have introduced bugs.
Factored code with Ltac's refine in Extratactics.
|
|
As simple as this looks, there's been some quite subtle issues in doing this modification, there may be bugs left.
|
|
|
|
|
|
|
|
|
|
The old implementation did not beta-iota normalize before observing the head of
the term, resulting in stange bugs.
|
|
|
|
|
|
|
|
the printing of the context of open evars in Check.
|
|
|
|
|
|
Check (see cfff8f8a327) [printing only visible evars, not the ones
corresponding to unrelated open goals + fixing bug on wrong sigma and
on evar_info normalization].
|
|
convert_concl/convert_hyp. This was actually probably the main source
of inefficiency introduced on Oct 9 (see e.g. CoLoR), rather than
nf_enter, as suspected in 3c2723f.
|
|
By moving convert_concl to new proof engine, re-typecheckeing was
incidentally introduced. Re-typechecking revealed that vm bug #2729
was still open. Indeed, the vm was still producing an ill-typed term.
This commit fixes ill-typedness of the vm in #2729 when reconstructing
a "match" in an inductive type whose constructors have let-ins.
Another part is still open (see test-suite).
|
|
but the internal representation dropped let-in.
Ideally, the internal representation of the "match" should use
contexts for the predicate and the branches. This would however be a
rather significant change. In the meantime, just a hack.
To do, there is still an extra @ in the constructor name that does not
need to be there.
|
|
|
|
committed by mistake. The message pretended to have a fix which is only
superficially a fix. The problem is more complex.
This reverts commit 251218905daea0838a3738466afa1c278bb3e81b.
|
|
équation;" which was committed by mistake.
This reverts commit a53b44aa042cfded28c34205074f194de7e2e4ee.
|
|
|
|
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.
|
