| Age | Commit message (Collapse) | Author |
|---|
|
due to cleared/reverted section variables.
This fixes the get_type_of but requires keeping information
around about the section hyps available in goals during resolution.
It's optimized for the non-section case (should incur no cost there),
and the case where no section variables are cleared.
|
|
|
|
This makes [refine] typecheck the term only once (instead of twice),
(Qed excluded of course). Fix test-suite file for output of constraints
accordingly.
|
|
|
|
Was PR#328: Change the order of arguments of fig2dev.
|
|
Was PR#233: [search] Search result streaming
|
|
|
|
If an existing evar was cleared in pretyping (typically while
processing "ltac:"), it created an evar considered as new. Updating
them instead along the "cleared" flag.
If correct, I suspect similar treatment should be done for refining
along "change", "rename" and "move".
|
|
|
|
The new algorithm produces different sets of arcs than in 8.5, hence
existing developments may fail to pass now because they relied on
the (correct but more approximate) result of minimization in 8.5 which
wasn't insensitive.
The algorithm works bottom-up on the (well-founded) graph to
find lower levels that an upper level can be minimized to. We
filter said lower levels according to the lower sets of the other levels
we consider. If they appear in any of them then we don't need their
constraints. Does not seem to have a huge impact on performance in HoTT,
but this should be evaluated further.
Adapt test-suite files accordingly.
|
|
|
|
Universe context not properly declared. Improve API
and code in declare.ml to allow declaration of universe contexts,
used by declaration of universes and constraints (separately).
|
|
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.
|
|
|
|
It now prints evars with candidates as well if there are any.
|
|
These variants are from 8.3 but were never documented except in CHANGES.
|
|
|
|
When trying different possible return predicates, returns the error
given by the first try, assuming this is the most interesting one.
|
|
|
|
|
|
The doc of auto hints now mention again that sometimes a hint
will be used with simple apply and sometimes it will be used
with exact.
It does not try to be fully precise in that we don't
necessarily want to document the behaviors of auto that
we might like to change.
See also the discussion on commit 9227d6e.
|
|
For some reason, with my version of transfig (which seems to be the latest),
the order of arguments of the fig2dev command matters: -L png must come
before -m 2. I suppose that this fix shouldn't break things for others.
|
|
|
|
In order to get proper coloring, we must tag the headers of error
messages in `CError`.
This should fix bug
https://coq.inria.fr/bugs/show_bug.cgi?id=5135
However, note that this could interact badly with the richpp printing
used by the IDE. At this level, we have no clue which tag we'd like to
apply, as we know (and shouldn't) nothing about the top level backend.
Thus, for now I've selected the console printer, hoping that the
`Richpp` won't crash the IDE.
|
|
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.
|
|
This way of giving the summary avoids redundancy as much as possible.
It is helpful for the auto-completion of Company-Coq of @cpitclaudel.
|
|
Now that this tactic has been fixed (commit 58d1381),
it needed to get documented.
|
|
PR#173 introduced a record field name clash in `stm.mli`, with duplicate
fields `start/stop` for the types `focus` and `static_block_declaration`.
We fix by renaming the younger ones (as to minimize code
incompatibilities), but other options are possible/could be preferred,
however they would be quite more invasive so I think they should be
postponed for the day the Stm API is cleaned up.
|
|
Improve the description of what auto/eauto do.
These two tactics rely on the simple version of apply/eapply.
Since this simple version is available to the end user,
it is better to mention it. See also the confusion that such
description can create in the thread "Understanding auto" on Coq-Club.
|
|
|
|
I do not know how to provide a proper test in 8.5, as the location on my
machine appears in the error printed when loading the file. Adding a Fail
on the End command does not help much either, because it simply does not
print anything.
Do not merge this commit in 8.6, we still want a test there.
|
|
The commit which caused the regression (5ea2539d4a) looks reasonable.
However, it happens that this commit made that unification started in
the #4955 example to follow a path with problems of the form
"proj ?x == ?x" which clearly are unsolvable (both ?x have the same
instance).
We hack the corresponding very permissive occur-check function so that
it is a bit less permissive.
One day, this occur-check function would have to be rewritten in a
more stricter way.
----------------------------------------------------------------------
Extra comments:
I could list several functions for occur check of evars.
Four of them are too strict in the sense that they do not take into
account occurrences of evars which may disappear by reduction, nor
evars which have instances made in such a way that the occur-check is
solvable (as in "fst ?x[y:=(0,0)] = ?x[y:=0]"). These are:
- Termops.occur_evar for clenv, evar_refiner, tactic unification
- syntactic check without any normalization, even on defined evars
- Evarutil.occur_evar_upto for refine and the V82 compatibility mode
- syntactic check without any normalization but inlining of defined evars
- Evarsolve.occur_evar_upto_types for evar_define
- syntactic check without any normalization but inlining of defined evars
- occur-check in the type of evars met
- optimization for not visiting several time the same evar
- Evarsolve.noccur_evar for pattern unification and for inversion of
substitution (evar/evar or evar/term problems)
- syntactic check without any normalization but inlining of defined evars
- occur-check in the type of evars met in arguments of projections
- occur-check in the type of variables met in arguments of projections
- optimization for not visiting several time the same evar
- optimization for not visiting several time the type of the same variable
- note: to go this way, it seems to me that it should check also in
all types which are a cut-formula in the expression
One is much too lax:
- Evarconv.occur_rigidly
- no recursive check except on the types of "forall" and sometimes
in the arguments of an application
- note: there is obviously a large room for refinements without
loosing solutions
|
|
This covers the case e.g. of "xₚ" (until the table of unicode
characters is upgraded!).
|
|
`Notation ".a" := nat.' was accepted and used for printing but not
recognized in parsing. Now it does. Other examples in test-suite.
|
|
The warning was pointless since the notation was accepted and parsed
anyway.
We now treat unrecognized unicode characters like ordinary
undefined tokens (e.g. "#" in a bare Coq).
For instance, "aₚ", or ".ₚ", or "?ₚ" now fail with "Undefined token"
rather than "Unsupported Unicode character".
|
|
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).
|
|
|
|
The fix solves the original bug report but it only turns the Not_found
into a normal error in the alternative example by Guillaume. See
test-suite file for comments on how to eventually improve the
situation and find a solution in Guillaume's example too.
|
|
|
|
|
|
The output was embedding local paths from my machine.
|
