| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |\| | | |
|
| | |\ \ \
| | | | |
| | | | |
| | | | | |
Was PR#366: Univs: fix bug 5208
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Parameter was implemented the wrong way trying to separate the universes
of the telescope.
|
| |\| | | | |
|
| | |/ / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Universes are kept in normal form w.r.t. equality but not the <=
relation, so the previous check worked almost always but was actually
too strict! In cases like (max(Set,u) = u) when u is declared >= Set it
was failing to find an equality. Applying the KISS principle:
u = v <-> u <= v /\ v <= u.
Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of
a colon in a typing judgment), this was not the case when an algebraic
universe instantiated an evar that appeared in the term. We force their
universe variable status to change in refresh_universes to avoid this.
Fix ind sort inference: Use syntactic universe equality for inductive
sort inference instead of check_leq (which now correctly takes
constraints into account) and simplify code
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Note: "dependant" does exist, but it is a noun and it means a person that
is somehow financially dependent on someone else.
|
| | | | |
| | | |
| | | |
| | | | |
#3339).
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing
changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341.
It turns out that calling from fake_ide the STM commands that were removed
by this PR requires an extension of the XML protocol. So postponing the
integration.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
I think these commands never make a lot of sense on scripts other than
debugging and we have better methods now.
The last remaining command, used for the tty emulation has been renamed
to VtBack, but it should go away at some point too once the legacy
interfaces are removed.
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Recalculating the metric all the time was proving costly (it was obvious
even on small queries).
|
| | | | |
| | | |
| | | |
| | | | |
Having more disctinc symbols incurs a penalty.
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | | |
This orders the results of search commands (such as `Search`,
`SearchAbout`, …) according to a "relevance" metric to minimise.
In this minimal version, the metric is the size of the displayed term.
|
| | |\ \
| | | |
| | | |
| | | | |
Was PR#339: Documenting type class options, typeclasses eauto
|
| | | | | |
|
| | |\ \ \
| | | | |
| | | | |
| | | | | |
Was PR#331: Solve_constraints and Set Use Unification Heuristics
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
Note that this is still broken when loading files containing C-zar scripts.
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
- The flags are now interpreted from left to right, without any other
precedence rule. The previous one did not make much sense in interactive
mode.
- Set Warnings and Set Warnings Append are now synonyms, and have the
"append" semantics, which is the most natural one for warnings.
- Warnings on unknown warnings are now printed only once (previously the
would be repeated on further calls to Set Warnings, sections closing,
module requiring...).
- Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced
to "-foo" (if foo exists, "" otherwise).
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Strangely enough, the checker seems to rely on an outdated decompose_app
function which is not the same as the kernel, as the latter is sensitive
to casts. Cast-manipulating functions from the kernel are only used on
upper layers, and thus was moved there.
|
| |\| | | | |
|
| | | |/ /
| |/| | |
|
| | |\ \ \
| | | | |
| | | | |
| | | | | |
Was PR#319: More error tagging, try to fix bug 5135
|
| | |\ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#337: Fix arguments
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
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.
|
| | |\ \ \ \ \
| | | |_|_|/
| | |/| | | |
|
| |\| | | | | |
|
| | | |_|_|/
| |/| | |
| | | | |
| | | | |
| | | | | |
reconsider_conv_pbs -> reconsider_unif_constraints
consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Conversion problems are in a de Bruijn environment that may
include references to unbound rels (because of the way evars
are created), we patch the env to named all de Bruijn variables
so that error printing does not raise an anomaly. Also fix a minor
printing bug in unsatisfiable constraints error reporting.
HoTT_coq_117.v tests all of this.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This patch converts the `search_*` functions to use an iter-style API.
Consequently, the Search Vernac will produce a message for each search
result, greatly improving roundtrip time as IDEs can effectively display
the results in a streaming way.
It also allows different printers to be used.
I didn't observe a performance difference (as things seem to be
dominated by printing and `Declaremods`).
As a minor tweak, we make search with "Output Name Only" more efficient.
Motivation:
-----------
Currently, the main search API `Search.generic_search` is an effectful,
iteration-based function:
```ocaml
val generic_search : int option -> display_function -> unit
```
This type is imposed by `Declaremods`, which exposes an effectful,
iteration-based API to traverse Coq library objects.
The `Search.search_*` functions try to offer a more functional API by
returning a list of pretty printing commands. They need to build an
internal intermediate list for that purpose.
However, this is a waste of time, as the destination of these lists is
to be flushed out by the printer right away.
|
| | | |_|/
| |/| |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The current tag system in `Pp` is generic, which implies we must choose
a tagging function when calling a printer.
For console printing there is a single choice, thus this commits adds it
a few missing cases.
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
It was not very useful as just parsing won't get you very far due to
lack of notation loading.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Given the current style in flags.mli no reason to have a function.
A deeper question is why a global flag is needed, in particular the use
in `interp/constrextern.ml` seems strange, the condition in the lexer
should be looked at and I'm not sure about `printing/`.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Also renaming vernac_com into interp_vernac and eval_expr into
process_vernac to clarify that it does side-effects (on the contrary
of Stm.interp/Vernacentries.interp).
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Moving set_formatter_out_channel where it naturally closes the
corresponding opening set_formatter_output_functions.
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This is not fully satisfactory though since we would not like to have
"eval_expr" depending on a parsing/lexing/comments state... but it
does because of eval_expr possibly printing the vernac expression
given to it.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
8a8caba3).
- Adding cLexer.current_file to the lexer state, i.e. making it a
component of the type "coq_parsable" of lexer state (it was
forgotten in b8ae2de5 and 8a8caba3).
- Inlining save_translator/restore_translator which have now lost most
of their substance.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
It was not used any more by coqdoc since b8194b22 (Dec 2010).
The table is now only part of the lexer function closure
(and only in the camlp5 case).
|
Pierre-Marie Pédrot
Maxime Dénès
Matthieu Sozeau
Guillaume Melquiond
Emilio Jesus Gallego Arias
Arnaud Spiwack
Hugo Herbelin
Cyprien Mangin
Matthieu Sozeau