| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
| |
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
(clause "where" with implicit arguments)
|
| | |_|_|/
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to
put any pattern in binders, prefixed by a quote."] its current
placement as well as the hook don't make a lot of sense.
In particular, they prevent parts of Coq working without linking the
parser.
To this purpose, we need to consolidate the `Constrexpr`
utilities. While we are at it we do so and remove the `Topconstr`
module which is fully redundant with `Constrexpr_ops`.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
To this purpose we allow plugins to register functions that will
modify the state.
This is not used yet, but will be used soon when we remove the global
handling of the proof state.
|
| | |/ /
|/| |
| | |
| | |
| | | |
As of Nov 2017, the standard number of entries is 85, it easily goes
up with some other plugins, so 211 seems like a good compromise.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
I followed what seems to be the intention of the code, with the
original intention of remove the global imperative proof state.
However, I fully fail to see why the new API is better than the old
one. In fact the opposite seems the contrary.
Still big parts of the "new proof engine" seem unfinished, and I'm
afraid I am not the right person to know what direction things should
take.
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| |/ / |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
PR #1120 was still buggy for the following reasons: variables in the
lhs of the notation were linked in the glob file while they have
nowhere to link to (the binder is the notation string) [I thought the
change I commited in links.html.out was actually improving but it was
an overlook, sorry.]
|
| | |
| |
| |
| | |
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)
|
| |\ \ \ \ \ \ |
|
Emilio Jesus Gallego Arias
Maxime Dénès
Hugo Herbelin
Gaëtan Gilbert
Matej Košík
Pierre-Marie Pédrot
Paul Steckler