| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
No other changes (long only because of a change of indentation).
|
| | |
|
| |
|
|
| |
Fixing : in Declare Module.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
"|]"" because this commit triggers a
Error: Files proofs/proofs.cma(Miscprint)
and /usr/local/lib/ocaml/compiler-libs/ocamlcommon.cma(Lexer)
make inconsistent assumptions over interface Lexer
Adding two extra spaces systematically instead.
This reverts commit 72be1f6beafafc3edd30df673fbb6c7e88f8fac7.
|
| |
|
|
| |
with user-level notations by inserting spaces.
|
| |
|
|
| |
exist as a keyword by inserting a space inbetween.
|
| |
|
|
| |
presence of entries starting with a non-terminal such as "b ^2".
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
implicit is found whether one writes (sig P) or {x|P x}.
|
| |
|
|
| |
VERNAC EXTEND.
|
| | |
|
| |
|
|
| |
implicit arguments when in beautification mode.
|
| |
|
|
|
|
| |
allows for a simpler re-printing of assert.
Also fixing the precedence for printing "by" clause.
|
| |
|
|
| |
does not print to ** which is a keyword.
|
| |
|
|
|
| |
calling Pcoq.parse_string, what some plugins such as coretactics, are
doing, thus breaking the beautification of "Declare ML Module").
|
| |
|
|
|
|
|
|
| |
with a clause where, nor Notation, nor Fixpoints.
Should be certainly improved at least for Inductive types and
Fixpoints, depending on whether there is a "where" clause for
instance.
|
| |
|
|
|
|
| |
beautification of the standard library.
Currently not intrusive but needs two extra phases of compilation.
|
| | |
|
| |
|
|
|
| |
computing the arguments which allows to decide which list of implicit
arguments to consider when several such lists are available.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
clause of a "match" over an irrefutable pattern.
|
| |
|
|
|
|
| |
in interning of patterns.
No semantic changes (except the type of ids_of_cases_indtype).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
variables" when matching over "{v : _ | _ & _}" which hides twice the
binding "fun v" since it is "sig2 (fun v => _) (fun v => _)".
Computing the bound variables statically at internalisation time
rather than every time at interpretation time. This cannot hurt even
if I don't know how to deal with the "notation" problem of a single
bound variable actually hiding two: at the current time, the notation
is printed only if the two variables are identical (see #4592), so,
with this semantics the warning should not be printed, but we lost the
information that we are coming from a notation; if #4592 were
addressed, then one of the binding should be alpha-renamed if they
differ, so collision should be solved by choosing the variable name
which is not renamed, but the matching algorithm should then be aware
of what the notation printing algorithm is doing... maybe not the most
critical thing at the current time.
|
| | |
|
| |\
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This branch mainly provides two features:
1. The resolution of tactic notation scopes is not tied to a hardwired Pcoq
registration anymore. We expose instead an API to interpret names as a given
generic argument, effectively reversing the logical dependency between parsing
entries and generic arguments.
2. ML tactics do not declare their own notation system anymore. They rely instead
on plain tactic notations, except for a little hack due to the way we currently
interpret toplevel values.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
Instead of relying on entry names as given by a hardwired registering
scheme in Pcoq, we recover them first through a user-defined map, and
fallback on generic argument names.
|
| | | |
|
| |/ |
|
| |\ |
|
| | | |
|
Hugo Herbelin
Pierre-Marie Pédrot