| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
This tactical is inspired by discussions on the Coq-club list. For now
it is still undocumented, and there is room left for design issues.
|
|
|
|
We retypecheck the hypotheses introduced by the refine primitive instead of
blindly trusting them when the unsafe flag is set to false.
|
|
|
|
its main interest!
|
|
|
|
|
|
This is not perfect though, some primitives are unsound, and some
higher-order API should use polymorphic functions so as not to depend
on a given level.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
allow reusability of the implementation throughout the Coq codebase.
We effectively feature a generalized version of the logical monad where the
input state, the output state and the inner exception can be arbitrarily chosen.
This will allow for more efficient implementations of close variants of the
monad.
|
|
Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.
As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.
|
|
progress.
Also compare goals up to evar instantiation (otherwise no progress would be observed when only unification occurs, unless some [nf_evar] is done). Performance look unchanged so far.
Some code from [Evd] which was used only in [tclPROGRESS] have been moved out (and [progress_evar_map] was now dead, so I killed it).
Fixes bugs (one reported directly on coqdev, and #3412).
|
|
|
|
|
|
Had to put some hook in the handler of Proofview.NoSuchgoals.
Documentation updated. CHANGE updated.
|
|
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
|
|
for typeclasses.
This was not the case for goals created at the end of the tactic by salvaging the [future_goals] from the evar map. It would cause typeclass resolution to try and solve these goals (if they have a class type) at each subsequent tactic.
Fixes #3841.
|
|
propagate it. This allows C-zar to continue to work.
Don't know if it is the best way to do it.
|
|
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.
|
|
The function initializing proofviews were marking all evars as non-resolvables
for the proofview, while only goal evars ought to be.
|
|
|
|
Closes #3801.
|
|
|
|
- drops all Defined entries from the evar map (applying the subst to the
initial evar and the undefined evars types).
- call Gc.compact
Now the question is: where should these two commands be documented?
|
|
|
|
|
|
The name is chosen in accordance to Ltac's syntax. In particular [refine] prints as Ltac's refine, which is not entirely correct (Ltac's refine does some βι-reduction after refinement). Maybe it would be better to give make it clear that it is a different refine. Still in refine, the constr is printed without taking into account the new evars, which, apart from potentially getting the order of the goals wrong, prints new evars as ?x instead of ?[x]. A printer for terms with new evars will be necessary.
In the case of [V82.tactic], the name is just <unknown> because there is no way to retrieve any information. It won't appear in the first level of info in Ltac, however, if the user would require a deeper trace, he may see internal tactics (Tactics defined with TACTIC EXTEND also have weird, unparsable, internal names).
|
|
Hence dispatches are printed as dispatches rather than sequences.
|
|
Called with [Info n tac], runs [tac] and prints its info trace unfolding [n] level of tactic names ([0] for no unfolding at all).
|
|
|
|
|
|
Otherwise I risked catching errors from the argument functions when I wanted to catch size mismatch to add information to errors.
|
|
9f51aafebd5f3a00dabfe056772a300830b3c430 )
|
|
future goals).
Fixes #3757. Thanks to Hugo for helping pinpoint the issue.
|
|
|
|
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.
|
