| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Porting them is still to be done, but at least we don't rely on the wrapper
everywhere.
|
|
Moving code around uncovered this bug.
|
|
|
|
It was only used at one point in the STM, and its localization was suprising
to say the least. Furthermore it was relying on legacy code. Instead we hardcode
it in the STM.
|
|
This function was used almost everywhere with the wrapper around.
|
|
Despite being marked as a breaking change by myself, it seems that the
underlying condition had been solved in the meantime.
|
|
|
|
Improve comments
|
|
Thread the `ev` (an `evar_flag`) appropriately through `intros0`.
Discussed on https://gitter.im/coq/coq?at=5eacace7f0377f16316083b8.
|
|
same inductive)
Numeral Notations now play better with multiple scopes for the same
inductive. Previously, when multiple numeral notations where defined
for the same inductive, only the last one was considered for
printing. Now, we proceed as follows
1. keep only uninterpreters that produce an output (first
List.map_filter)
2. keep only uninterpretation for scopes that either have a scope
delimiter or are open (second List.map_filter)
3. the final selection is made according to the order of open scopes,
(find_uninterpretation) or or according to the last defined
notation if no appropriate scope is open (head of list at the end)
|
|
Ack-by: JasonGross
Ack-by: jfehrle
|
|
As per https://github.com/coq/coq/pull/12197#discussion_r418480525 and
https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef
|
|
Note that this slightly changes the semantics of backtracking across
`start ltac profiling`.
|
|
Fixes #12196
|
|
This new primitive (which could be implemented in terms of `tclCASE`,
but which I believe encapsulates a useful unit of behavior) is needed
for correctly implementing both `with_strategy` and for implementing
multi-success support for the Ltac Profiler.
The basic function of this tactical is to allow wrapping multi-success
tactics with initialization and cleanup routines. For example, if `tac`
is a multi-success tactic that writes its status to a log file, you
might want to wrap `tac` in "first open the log file" and then after it
runs "finally close the log file". (Unfortunately, the way the monad is
set up doesn't allow passing data from the most recent run of the
initializer to the tactic, which suggests that perhaps there's something
a bit off about this abstraction. Perhaps we should set up a ref cell
and that will hold the most recent return of the initializer and pass
this ref cell to the wrapped tactic? But this can be done externally
without needing to modify the current API. In any case, such data is
not needed in the case of the Ltac Profiler, where the initializer is
"update the current call stack and record the current start time" and
the finalizer is "update the call stack and record the end time", and
you want to have the start time be restarted when re-entering a tactic.
Nor is it needed for `with_strategy` which needs to update the global
conv_oracle so that it plays nicely with `abstract`.)
|
|
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
Also including feedback from Enrico Tassi.
|
|
|
|
This is to be compatible with the possibility of having non truly
recursive fixpoints.
|
|
There was also a non truly recursive in the doc.
|
|
|
|
remove itself in the set of elements bigger than it if it is indeed
the case.
This does not impact the warning issued when the recursivity is not
mutual but this produces a result consistent with the unary case when
the order is reflexive (i.e. results of the form (x,Inr[x,y]) happens
also in the mutual case to indicate a cycle x<=y<=x while before we
had results of the form (x,Inr[x]) only in the unary case). I.e.:
Before:
(x,[y]),(y,[x]) -> (x,Inr[]),(y,Inl x)
(x,[x]) -> (x,Inr[x])
Now:
(x,[y]),(y,[x]) -> (x,Inr[x]),(y,Inl x)
(x,[x]) -> (x,Inr[x])
|
|
|
|
Reviewed-by: MSoegtropIMC
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
