| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
Objects registered through the callback functions were pushed on the libstack
before the ML-MODULE object itself, leading to anomalies when the corresponding
object was assuming that the ML module was properly defined in any other Coq
module requiring the Declare ML command.
|
|
|
|
|
|
|
|
This reverts commit 466b7e69e49a5f4bba36b834a2e046f120ece07c.
|
|
We protect the code against the presence of pattern casts where they are
not supported. Why we cannot make the pattern type reflect this is
a long story (described in this commit), but in the long term we
probably want to support them anywhere, like OCaml does. Of course, it
will require to adjust the pattern matching compiler.
|
|
Also getting rid of a global side-effect.
|
|
This is a bit ad-hoc, but looks better for warnings since there is
a command-line flag accepting the same values, so comma will lead to
fewer parsing issues than space.
|
|
Was PR#305: A possible solution to the issue of fine-tuning warnings in
script.
|
|
|
|
Was PR#263: Fast lookup in named contexts
|
|
|
|
Was PR#304: fixing bug 4609
|
|
between proofs in tactic injection, with a side-effect on inversion.
|
|
|
|
|
|
That way, bullet detection no longer depends on a global variable
indicating whether a line is starting. This causes a small change in the
recognized language. Before the commit, "--++" was recognized as a bullet
"--" followed by a keyword "++" when at the start of a line; now it is
always recognized as a keyword "--++".
This also fixes a bug in Tok.to_string as a side-effect.
|
|
|
|
|
|
The patch is quite dumb: it essentially consists in alpha-renaming bound
module names when printing a functor, by checking that the name was not
already present, and generating a fresh one otherwise.
|
|
The blacklist set was converted into a string list for each item in the
environment during a search. In fact, the blacklist was checked for
each item, even if the item was already known to be ultimately discarded.
This commit fixes both performance issues. First, blacklist_filter is no
longer used directly but in two stages. Second, the boolean values are
no longer computed before calling the shortcutting operators. It seems
like someone had already noticed part of the second issue, since some (but
not all) of the boolean values were lazily computed.
The speed up becomes noticeable when the blacklist set contains more than
four elements.
|
|
This does not affect the semantics of these functions.
|
|
For now, the only meaningful user is "Set Warnings". Example:
Section Bar.
Local Set Warnings Append "-foo".
(* warning foo is now disabled *)
End Bar.
(* foo is now reenabled, assuming it was before entering the section *)
|
|
Whether an option should be set or appended to is stored as a 2-value
flag next to the new content. This commit also cleans the code by
declaring a single object for each persistent option rather than three
different ones (one per locality).
|
|
|
|
|
|
This bug was introduced by 37ab45726, because the new apply_type function
was not checking that the new goal was indeed well-typed. We add this check
locally in the generalize dependent tactic.
|
|
|
|
Order of items made stable
|
|
Was PR#303: LtacProf cutoff is for total percent, not time
|
|
Was PR#299: Fix bug #4869, allow Prop, Set, and level names in
constraints.
|
|
|
