| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
When a notation was starting or ending a space, Coq assumed the notation
had no terminal symbol in either places. Coq also considered a notation
containing only spaces to be productive. As stated in the documentation,
extraneous spaces are only meant as printing hints, they are not meant to
have any influence on parsing.
|
| | |
| |
| |
| | |
This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Notation "## c" := (S c) (at level 0, c at level 100).
which break the stratification of precedences. This works for the case
of infix or suffix operators which occur in only one grammar rule,
such as +, *, etc. This solves the "constr" part of #3709, even though
this example is artificial.
The fix is not complete. It puts extra parenthesese even when it is
end of sentence, as in
Notation "# c % d" := (c+d) (at level 3).
Check fun x => # ## x % ## (x * 2).
(* fun x : nat => # ## x % (## x * 2) *)
The fix could be improved by not always using 100 for the printing
level of "## c", but 100 only when not the end of the sentence.
The fix does not solve the general problem with symbols occurring in
more than one rule, as e.g. in:
Notation "# c % d" := (c+d) (at level 1).
Notation "## c" := (S c) (at level 0, c at level 5).
Check fun x => # ## x % 0.
(* Parentheses are necessary only if "0 % 0" is also parsable *)
I don't see in this case what better approach to follow than
restarting the parser to check reversibility of the printing.
|
| | |
| |
| |
| |
| | |
could be used with arguments which are binding variables, as was done
in ssrfun.v.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- Making a clear distinction between expressions of the notation which
are associated to binding variables only (as in `Notation "'lam' x ,
P" := (fun x => P)" or `Notation "'exists2' x : t , p & q" := (ex2
(fun x:t => p) (fun x:t => q))') and those which are associated to
at list one subterm (e.g. `Notation "x .+1" := (S x)' but also
"Notation "{# x | P }" := (ex2 _ (fun y => x = F y) (fun x => P))'
as in #4592). The former have type NtnTypeOnlyBinder.
- Thus avoiding in particular encoding too early Anonymous as GHole
and "Name id" as "GVar id".
There is a non-trivial alpha-conversion work to do to get #4592
working. See comments in Notation_ops.add_env.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
We simply handle the "break" in error messages. Not sure it is the
proper bugfix though, we may want to be able to add breaks in such
recursive notations.
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
Actually the identifier was never used and just carried along.
|
| | |
| |
| |
| |
| | |
The TacAlias node now only contains the arguments fed to the tactic notation.
The binding variables are worn by the tactic representation in Tacenv.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This commit has deep consequences in term of tactic evaluation,
as it allows to pass any tac_arg to ML and alias tactics rather than
mere generic arguments. This makes the evaluation much more uniform,
and in particular it removes the special evaluation function for notations.
This last point may break some notations out there unluckily.
I had to treat in an ad-hoc way the tactic(...) entry of tactic notations
because it is actually not interpreted as a generic argument but rather
as a proper tactic expression instead.
There is for now no syntax to pass any tactic argument to a given ML or
notation tactic, but this should come soon.
Also fixes bug #3849 en passant.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| |\|
| |
| |
| |
| |
| |
| | |
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The solution is a bit ugly. In order for two tactic notations identifiers not
to be confused by the inclusion from two distinct modules, we embed the name of
the source module in the identifiers. This may still fail if the same module is
included twice with two distinct parameters, but this should not be possible
thanks to the fact any definition in there will forbid the inclusion, for it
would be repeated. People including twice the same empty module otherwise
probably deserve whatever will arise from it.
|
| |\| |
|
| | |
| |
| |
| | |
This reverts commit 124734fd2c523909802d095abb37350519856864.
|
| |\| |
|
| | |
| |
| |
| |
| | |
This is a fixup of commit 2e09a22b that used uniquely generated kernel names
but forgot to substitute them.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| | |
This reverts commit 2e09a22baeb93c57e6d8388313dc638349679910.
|
| | | |
|
| |/
|
|
|
| |
This will allow to get rid of the fragile mechanism of discriminating which
entry to call depending on the dynamic type of its arguments.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
| |
+ consequences of this check on the standard library (moved the no-op
in Notation modifiers to what there were supposed to do; these are
anyway local notations, so compatibility is safe - please AS or PL,
amend if needed).
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
so that one can retrieve them and pass them to third party tools (i.e.
print the AST with the notations attached to the nodes concerned).
Available syntax:
- all in one:
Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2").
- a posteriori:
Format Notation "a /\ b" "latex" "#1 \wedge #2".
|
| | |
|
| |
|
|
|
|
| |
ML tactics that may be used as simple identifiers are now declared as
a true Ltac entry pertaining to the module that contains the Declare ML
Module statement.
|
| |
|
|
|
| |
Also taking advantage of the change to rename it into TacML. Ultimately
should allow ML tactic to return values.
|
| |
|
|
| |
potentially conflicting tactics names from different plugins.
|
| | |
|
Pierre-Marie Pédrot
Guillaume Melquiond
Hugo Herbelin
Maxime Dénès
Lionel Rieg
Enrico Tassi