| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
| |
Instead of circumventing the problem on the caller's side, as was done
in Arguments, we simply avoid failing as there was no real reason for
this anomaly to be triggered. If the list of renamings is shorter than
the one of implicits, we simply interpret the remaining arguments as not
renamed.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The main point of this change is to fix #3035: Avoiding trailing
arguments in the Arguments command, and related issues occurring in
HoTT for instance. When the "assert" flag is not specified, we now
accept prefixes of the list of arguments.
The semantics of _ w.r.t. to renaming has changed. Previously, it meant
"restore the original name inferred from the type". Now it means "don't
change the current name".
The syntax of arguments is now restricted. Modifiers like /, ! and
scopes are allowed only in the first arguments list.
We also add *a lot* of missing checks on input values and fix various
bugs.
Note that this code is still way too complex for what it does, due to
the complexity of the implicit arguments, reduction behaviors and renaming
APIs.
|
|
|
|
|
| |
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.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Enablnig them would give a system that tells the user to replace e.g.:
le_n_Sn with Nat.le_succ_diag_r
lt_S with Nat.lt_lt_succ_r (on other types like R and and positive, the same
lemma is called lt_lt_succ)
In many cases, the new names will be too painful for intensive users.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Evarconv was made precociously dependent on user-declared reduction
behaviors. Only cbn should rely on that.
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | | |
This change exposed bug #4763
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This option was not doing anything... Today, one can turn the
compatibility notations warning into an error, if ever that was the
intended semantics.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
These warnings can now be configured like any other, so we don't need
a specific option anymore.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Do not force all remaining conversions problems to be solved after the
_first_ solution of an evar, but only at the end of assignment of terms
to evars in w_merge. This was hell to track down, thanks for the help of
Maxime. contribs pass and HoTT too.
|
| | | | |
| | | | |
| | | | |
| | | | | |
A file was introduced by mistake in theories/Logic.
|