| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
We do up to `Term` which is the main bulk of the changes.
|
| |
|
|
| |
This will allow to merge back `Names` with `API.Names`
|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | | |
This is a first step towards some of the solutions proposed in #6008.
|
| | |/
| |
| |
| | |
Syntax removed in faa064c746e20a12b3c8f792f69537b18e387be6
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Originally, it was not possible to define a new vernacular command
in the following way:
VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY
[ "SomeCmd" ] -> [ Feedback.msg_notice ?loc (Pp.str "some message") ]
END
because "loc : Loc.t" was not bound.
This commit fixes that, i.e. the location of the custom Vernacular command
(within *.v file) is made available as "loc" variable bound on the right side
of "->" .
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
ML level can set the flags themselves.
In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".
This fixes bug #5281.
|
| |/ |
|
| |\
| |
| |
| | |
clause of an inductive definitions
|
| | |
| |
| |
| |
| |
| |
| | |
Users need to be careful wrt global state modification outside
`Vernacentries` without registering the functions.
In particular, our fail implementation also has to invalidate the cache.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We make Vernacentries.interp functional wrt state, and thus remove
state-handling from `Future`. Now, a future needs a closure if it
wants to preserve state.
Consequently, `Vernacentries.interp` takes a state, and returns the
new one.
We don't explicitly thread the state in the STM yet, instead, we
recover the state that was used before and pass it explicitly to
`interp`.
I have tested the commit with the files in interactive, but we aware
that some new bugs may appear or old ones be made more apparent.
However, I am confident that this step will improve our understanding
of bugs.
In some cases, we perform a bit more summary wrapping/unwrapping. This
will go away in future commits; informal timings for a full make:
- master:
real 2m11,027s
user 8m30,904s
sys 1m0,000s
- no_futures:
real 2m8,474s
user 8m34,380s
sys 0m59,156s
|
| | |
| |
| |
| |
| | |
We still don't thread the state there, but this is a start of the
needed infrastructure.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
We place `Proof_using` in the proper place [`vernac`] and we remove
gross parsing hacks.
The new placement should allow to use the printers and more convenient
structure, and reduce strange coupling between parsing and internal
representation.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Also add an output test for Suggest Proof Using.
This changes the .aux output: instead of getting a key
>context_used "$hyps;$suggest"
where $hyps is a list of the used hypotheses and $suggest is the
;-separated suggestions (or the empty string if Suggest Proof Using is
unset), there is a key
>context_used "$hyps"
and if Suggest Proof Using is set also a key
>suggest_proof_using "$suggest"
For instance instead of
112 116 context_used "B A;A B;All"
we get
112 116 context_used "B A"
112 116 suggest_proof_using "A B;All"
|
| |\ \ |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | | |
More dependencies / linking fixes.
|
| |\ \ \ \
| |_|/ /
|/| | |
| | | | |
printing-ony Notations
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
inductive definition)
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
to escape non-UTF-8 file names)
|
| | | | | | | | |
|
| | | | | |_|/
| | | |/| |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This allows e.g. the following to work:
Reserved Notation "* a" (at level 70).
Inductive P {n : nat} : nat -> Prop := c m : *m where "* m" := (P m).
We seize this opportunity to make main calls to Metasyntax to depend
on an arbitrary env rather than on Global.env.
Incidentally, this fixes a little coqdoc bug in classifying the
inductive type referred to in the "where" clause.
|
| | |_|_|_|/
|/| | | | |
|
| |\ \ \ \ \ |
|
| | |_|_|/ /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.
Next step, understand why.
|
| |/ / / /
| | | |
| | | |
| | | |
| | | | |
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
| |\ \ \ \ |
|
| | | | | | |
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
inductive types)
|
| |\ \ \ \ \ \ |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
The point is to emphasize stronglier when we are talking about
contexts or about arguments.
|
| | |/ / / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | | |
The number of effective parameters was used where the number of
declarations in the signature of parameters should have been used.
|
| | | | | | | |
|
| | | | | |/
| | | | |
| | | | |
| | | | |
| | | | | |
Call to nf_betaiota was done on one side of the comparison preventing
the same message to be repeated twice but not on the other side.
|
| |\ \ \ \ \ |
|
| | |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
An incoming commit is removing some toplevel-specific global flags in
favor of local toplevel state; this commit flags `Flags` use so it
becomes clearer in the code whether we are relying on some "global"
settable status in code.
A good candidate for further cleanup is the pattern:
`Flags.if_verbose Feedback.msg_info`
|
| |/ / / / |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
evd: Move constrain_variables to an operation on UState
Necessary to check universe declarations correctly for deferred proofs
in particular.
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
|
| | | | |
|
| |/ / |
|
| |\ \
| | |
| | |
| | | |
top of the linking chain.
|
| |\ \ \
| | | |
| | | |
| | | | |
from location in file
|
Emilio Jesus Gallego Arias
Maxime Dénès
Gaëtan Gilbert
Matej Košík
Hugo Herbelin
Pierre-Marie Pédrot
Paul Steckler
Matthieu Sozeau