| Age | Commit message (Collapse) | Author |
|---|
|
The output was embedding local paths from my machine.
|
|
I've messed up with parts of the compatibility files I had to commit.
|
|
|
|
branches (see PR #323).
|
|
|
|
|
|
|
|
We simply explicit that the type is actually referring to the return type,
not to the type of the argument of the pattern-matching. Note that the
heuristic could be enhanced so as to use the same code in both let-style
and match-style pattern-matching, but I'm leaving this for another time.
|
|
When printing evar constraints, we ensure that every variable from the
rel context has a name.
|
|
There was a catch-all clause in the tclORELSE0 function. We now only
catch noncritical exceptions.
|
|
|
|
This is more precise and probably clearer (see e.g. thread
"Understanding auto" on coq-club).
|
|
Revert "Inference of return clause: giving uniformly priority to "small inversion"."
This reverts commit 980b434552d73cb990860f8d659b64686f6dbc87.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This happens when recursive notations are used to define recursive
notations.
|
|
Was PR#286: Fix the definition of if_then_else for tactics with multiple
success.
|
|
|
|
git worktrees have a .git file instead of a .git directory.
Using Sys.file_exists is a more general solution which gives true in both cases.
|
|
|
|
But maybe it is that how the "Test" message is elaborated is not
intuitive...
|
|
|
|
(It should apply also interactively.)
|
|
|
|
|
|
Previously, some splipped through and were caught by unrelated calls to
typeclass resolution.
|
|
The move to systematically trying small inversion first bumps
sometimes as feared to the weakness of unification (see #5107).
----
Revert "Posssible abstractions over goal variables when inferring match return clause."
This reverts commit 0658ba7b908dad946200f872f44260d0e4893a94.
Revert "Trying an abstracting dependencies heuristic for the match return clause even when no type constraint is given."
This reverts commit 292f365185b7acdee79f3ff7b158551c2764c548.
Revert "Trying a no-inversion no-dependency heuristic for match return clause."
This reverts commit 2422aeb2b59229891508f35890653a9737988c00.
|
|
side_effects. Partial solution to the handling of side effects
in proofview.
|
|
I wrongly moved call to the function interpreting commands within a
different try-with block in 8a8caba36e.
|
|
|
|
In `Ftactic` the number of results could desynchronise with the number
of goals when some goals were solved by side effect in a different
branch of a `DISPATCH`.
See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).
|
|
|
|
More precisely, commands that calls parse_entry put the lexer in an
inconsistent state, breaking the lexing of bullet which relies on it.
(Not to be pushed to v8.6 which has a better fix).
|
|
done by the Ppcmd_comment token) and so that lexing/parsing
side-effects are collected at the same place, i.e. in CLexer.
|
|
the state of parsable streams, so that different lexing/parsing
processes can be started independently without conflicting.
Note however that these different lexing/parsing processes cannot be
run concurrently as they still work on the same piece of global memory
(i.e. calls to entry_parse should remain atomic). To go further, one
would typically need to be able to functionally pass the lexing state
to each call to the lexer.
Note that currently the beautifier is also running in the context of a
lexer/parser state (for the mapping of location to comments).
In particular, this fixes #5102 (parsing/lexing of bullets depending on
the lexing state which was global).
|
|
|
|
|
|
|
|
|
|
|
|
We defactorize the in_clause grammar entry to allow parsing of the "symmetry"
tactic when it has no arguments. Beforehand, the clause_dft_concl entry
accepted the empty stream, preventing the definition of symmetry as a mere
identifier.
|
|
We simply catch the RetypeError raised by the retyping function and translate
it into a user error, so that it is captured by the tactic monad instead of
reaching toplevel.
|
|
|
|
This was introduced to implement the Append feature on options. As usual when
messing with predefined keywords, this broke code in the wild. In order not
to create a new keyword, we do the string analysis on the production branch of
parsing.
|
|
#4363)."
This reverts commit 11ccb7333c2a82d59736027838acaea2237e2402.
This fixes bug #4874. We fallback to the original error message of v8.4.
The fallback printer introduced in this commit only gave unqualified names,
which is what this bug reports.
|
