| Age | Commit message (Collapse) | Author |
|---|
|
|
|
there is no focused goal.
The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not.
|
|
|
|
This was due to the unqualified uses of "Lazy" being disambiguated in different manners. I just changed the constructor name to "Select".
Fixes #3877.
|
|
[multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well.
|
|
I added a emacs_logger.
Still need to cleanup std_logger.
|
|
|
|
|
|
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.
|
|
[tryif t then t2 else t3] behaves like [t;t2] if [t] has at least one success, or [t3] otherwise. It generalises [t||t3] as failures from [t2] will not be caught.
|
|
You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
|
|
redex.
|
|
pattern-matching predicate.
|
|
is not defined while X_rect is, for example in HoTT/Coq.
|
|
|
|
As their commit messages suggested it, these commits were not intended
to be committed at this time. They are part of a on-going merge of the
code of induction and functional induction. Together with the fix
here, they are supposingly transparent, semantically speaking.
|
|
[Proofview].
The primitives in [Tacticals] respect Ltac's error level, whereas the one in [Proofview] do not necessarily. In that case the error caught was ignored causing arbitrary error level after [constructor] to be canceled.
Needed the addition of an [ORD] variant to [OR] in [Tacticals.New] to avoid unnecessary precomputation (the 'D' stands for 'delay').
Fixes #3838.
|
|
|
|
|
|
|
|
|
|
propagate it. This allows C-zar to continue to work.
Don't know if it is the best way to do it.
|
|
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.
|
|
- Registering strict implicit arguments systematically (35fc7d728168)
- Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6)
- Fixing Coq compilation (894a3d16471)
Systematically computing strict implicit arguments can lead to big
computations, so I suspend this attempt, waiting for improved
computation of implicit arguments, or alternative heuristics going
toward having more conversion in rewrite.
|
|
in tactic unification.
|
|
|
|
at least when f is an evaluable reference.
|
|
when the arguments of a constructor can be moved at the place of the
variable on which destruct or induction applies.
|
|
a UserError to ease debugging.
|
|
|
|
- removed the encapsulation in a Tactic Failure (I don't see why
setoid_rewrite should specifically raise a Fail - do I miss something?)
- avoid having twice a "Unable to satisfy ... constraints" message.
|
|
|
|
|
|
quantified hypothesis in functional induction. This has apparently no
visible effect, probably because functional schemes do not have
non-dependent hypothesis in their branches besides induction
hypotheses which are anyway introduced at the top of the context.
|
|
|
|
anymore since "destruct eq_dec" works like "destruct (eq_dec _ _)".
|
|
of the function are dependent.
|
|
|
|
|
|
|
|
|
|
|
|
Before this patch, when tactics-in-terms were relying on the ugly environment-
modifying primitives such as tclABSTRACT, the returned term was ill-typed
because the resulting effects were just dropped. Now we modify the returned
term on the fly, effectively getting rid of the effects it may depend on.
Yet, this is not completely satisfactory, because the tactic may solve some
goals at distance (I would have said by side-effect, but this is ambiguous
here). If ever the resulting terms are depending on the side-effects of the
tactic, then we are still unsound.
This patch should handle most of the use-cases gracefully. To really solve this
issue, we should rewrite the pretyper in the new monad, which is easier said
than done.
|
|
by commit bf0185694.
|
|
|
|
|
|
|
