| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: gares
Ack-by: herbelin
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
Ack-by: ejgallego
|
|
them more stable.
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
|
|
Contrarily to the comments, Coq_config.date was not the "release date" but
just another "compile date".
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
|
|
We also spill (some) non-generic arguments and initialization code
out of coqargs and to coqtop, namely colors for the terminal. There are
more of these, left to later commits.
|
|
This component holds the code for initializing Coq:
- parsing arguments not specific to the toplevel
- initializing all components from vernac downwards (no stm)
This commit moves stm specific arguments parsing to stm/stmargs.ml
|
|
|
|
|
|
|
|
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
Co-authored-by: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
|
|
|
|
Reviewed-by: herbelin
Ack-by: gares
Ack-by: ejgallego
|
|
Add menu item that uses this
|
|
An h-box inhibits the breaking semantics of any cut/spc/brk in the
enclosed box.
We tentatively replace its occurrence by an h or hv, assuming in
particular that if the indentation is not 0, an hv box was intended.
|
|
|
|
|
|
|
|
|
|
Before this patch, the proof engine had three notions of shelves:
- A local shelf in `proofview`
- A global shelf in `Proof.t`
- A future shelf in `evar_map`
This has lead to a lot of confusion and limitations or bugs, because
some components have only a partial view of the shelf: the pretyper can
see only the future shelf, tactics can see only the local and future
shelves. In particular, this refactoring is needed for #7825.
The solution we choose is to move shelf information to the evar map, as
a shelf stack (for nested `unshelve` tacticals).
Closes #8770.
Closes #6292.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
This is in preparation for the next commit which will clean-up the
current API flow in `Declare`.
|
|
|
|
|
|
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
The parsing rules defining classes of lexemes in language
configuration expect a Coq document and are not relevant in the
message and proof window. Thus backtracking on this part of #12169.
Keeping the highlighting style though.
|
|
This hopefully fix the segfaults we observe with completion.
|
|
Reviewed-by: ppedrot
|
|
It was previously only applied to the script buffer.
|
|
|
|
We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]
Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.
|
|
The iterator of the completion context does not seem trustable.
|
|
Let's see if it fixes #11943. See there for explanations about the
related segfault.
|
|
parsing of coqtop arguments in coqide
Reviewed-by: ejgallego
|
|
The completion proposals need to be ordered by length first for usability.
I aknowledge that it's too easy to mess up when refactoring, but here there was
a clear comment that this change should not have been performed.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Ack-by: ppedrot
|
|
|
|
Reviewed-by: ppedrot
|
|
Add headers to a few files which were missing them.
|
|
This is at least to be able to use spaces in file names (#11595).
In practice it protects also \, ', ", and many other symbols.
|
|
This encodes/decodes a list of string into a string in a way
compatible with shell interpretation. On the contrary of
Filename.quote which is for computer consumption, it introduces quotes
for human consumption.
The strategy is to split each string into substrings separated by
simple quotes. Each substring is surrounted by single quotes if it
contains a space. Otherwise, each backslash in the substring is
doubled. The substrings are concatenated separated by
backslash-protected single quote. The strings are then concatenated
separated with spaces. The decoding is shell-like in the sense that it
follows the rules of single quote, backslash and space.
|
