| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
non-recursive notations (#4815).
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
conversion on closed terms.
This will be useful to discriminate problems involving the "with"
clause and which fails by lack of information or for deeper reasons.
|
| | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | |
|
| | | | | | | | | | | |
|
| | |_|_|_|_|_|/ / /
|/| | | | | | | | |
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
By default we enable only {} and par: that are detectable in
a complete way.
|
| | |_|_|/ / / / /
|/| | | | | | | |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Tactic Notation "f" constr(x) := apply x. Ltac g x := f x.
Goal False.
g I. (* Was printing Top.Top#<>#1 *)
idtac; f I. (* Was not properly locating error *)
This is a "a minima" fix.
This a different fix than in trunk, so the merge will have to take the
trunk version.
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
https://github.com/coq/coq/pull/150#issuecomment-219141596
```bash
git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i
```
|
| | |_|/ / / / /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This add LtacProfiling. Much of the code was written by Tobias Tebbi
(@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq
v8.5 and Coq trunk.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
For Drop for example.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
The command line option is named:
- async-proofs-delegation-threshold
Values are of type float, default 1.0 (seconds).
Proofs taking less that the threshold are not delegated to
a worker.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This reverts commit a66b57ba4bba866bb626bde2b6fe3b762347eb3e.
|
| | |_|/ / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
- In Program, a check_evars_are_solved was introduced
too early. Program does it's checking of evars by itself.
- In Function, the universe environments were not threaded
correctly.
|
| | | | |_|/
| | |/| | |
|
| | | | | | |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The -o option lets one put .vo or .vio files in a directory of choice,
i.e. decouple the location of the sources and the compiled files.
This ease the integration of Coq in already existing IDEs that handle
the build process automatically (eg Eclipse) and also enables one to
compile/run at the same time 2 versions of Coq on the same sources.
Example: b.v depending on a.v
coq8.6/bin/coqc -R out8.6 Test src/a.v -o out8.6/a.vo
coq8.6/bin/coqc -R out8.6 Test src/b.v -o out8.6/b.vo
coq8.7/bin/coqc -R out8.7 Test src/a.v -o out8.7/a.vo
coq8.7/bin/coqc -R out8.7 Test src/b.v -o out8.7/b.vo
|
| | | | | |
|
| | | | | |
|
| |\ \ \ \
| | |/ /
| |/| | |
|
| | | | |
| | | |
| | | |
| | | | |
obligations".
|
| | | | | |
|
| | | | | |
|
| |\| | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
Also register properly the kind of definition.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | | | |
| | | |
| | | |
| | | | |
This reverts commit f2192b492ca5407e740cf9d9d8696da89c978b93.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
calling Pcoq.parse_string, what some plugins such as coretactics, are
doing, thus breaking the beautification of "Declare ML Module").
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | | |
- This patch changes the search interface to take [Str.regexp]s,
[constr_pattern]s, and [DirPath.t] instead of [string]s and
[string list]s.
- Convenience functions are provided to do the translation.
|
| |\| | |
|
| | | |
| | |
| | |
| | | |
so that they are not silently computed when not in debugging mode.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Falling back to the global setting if not given.
Useful to make Add Morphism fail correctly when the given proof terms
are incomplete. Adapt test-suite file #2848 accordingly.
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
defs in Print Assumptions"
|
| | |/| | |
|/| | | |
| | | | |
| | | | | |
into JasonGross-trunk-function_scope
|
| |\ \ \ \ \
| | |_|/ /
| |/| | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
could be used with arguments which are binding variables, as was done
in ssrfun.v.
|
| | | | | |
| | | | |
| | | | |
| | | | | |
The user-provided sort was ignored for them.
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Some parts of Evarutils were related to the management of evars under constraints.
We put them in the Evardefine file.
|
| | | | | | |
|
| |\| | | | |
|
Hugo Herbelin
Pierre-Marie Pédrot
Enrico Tassi
Jason Gross
Matthieu Sozeau
Emilio Jesus Gallego Arias
Matthieu Sozeau
Guillaume Melquiond
Gregory Malecha
Matej Kosik