| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
We artificially restrict the syntax though, because it is unclear of
what the semantics of several axioms in a row is, in particular about the
resolution of remaining evars.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- "Proof using p*" means: use p and any section var about p.
- Simplify the grammar/parser for proof using <expression>.
- Section variables with a body (let-in) are pulled in automatically
since they are safe to be used (add no extra quantification)
- automatic clear of "unused" section variables made optional:
Set Proof Using Clear Unused.
since clearing section hypotheses does not "always work" (e.g. hint
databases are not really cleaned)
- term_typing: trigger a "suggest proof using" message also for Let
theorems.
|
| | |
| |
| |
| |
| | |
There is no such thing as the OPTSEP macro in Camlp4 so I had
to expand it by hand.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This option disallows "declare at first use" semantics for universe
variables (in @{}), forcing the declaration of _all_ universes appearing
in a definition when introducing it with syntax Definition/Inductive
foo@{i j k} .. The bound universes at the end of a definition/inductive
must be exactly those ones, no extras allowed currently.
Test-suite files using the old semantics just disable the option.
|
| |\| |
|
| | |
| |
| |
| |
| | |
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
|
| |\| |
|
| | |
| |
| |
| | |
This (at least technically) solves the issue #4113 (see also #4329).
|
| |\| |
|
| | |
| |
| |
| |
| | |
The file seems to have been reintroduced by error by commit 012fe1a96, but
it was not compiled anyway.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| | |
A possible script breakage can occur if one has a notation
at level 11 that is also right associative (now 11 is left associative).
Thanks Georges for debugging that.
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| | |
"Conjecture" (see #4252).
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| | |
The command [Redirect "filename" (...)] redirects all the output of
[(...)] to file "filename.out". This is useful for storing the results of
an [Eval compute], for redirecting the results of a large search, for
automatically generating traces of interesting developments, and so on.
|
| | |
| |
| |
| |
| |
| | |
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
|
| | |
| |
| |
| | |
them (e.g. "fun ... ⇒ ...") factor well (see #2268).
|
| |\| |
|
| | | |
|
| | |
| |
| |
| | |
This is necessary to make ssr compile with both camlp4/5
|
| | | |
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
fresh now accepts a qualid, and behaves as if given the short name.
Since fresh used to accept an id, supporting qualid is IMO not a new
feature but just a fix. Hence the fix in v8.5.
|
| |\| |
|
| | |
| |
| |
| | |
Of course such proofs cannot be processed asynchronously
|
| |\| |
|
| | | |
|
| |/
|
|
|
| |
This will allow to get rid of the fragile mechanism of discriminating which
entry to call depending on the dynamic type of its arguments.
|
| | |
|
| |
|
|
|
|
| |
there is no focused goal.
The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not.
|
| |
|
|
|
|
| |
This was due to the unqualified uses of "Lazy" being disambiguated in different manners. I just changed the constructor name to "Select".
Fixes #3877.
|
| |
|
|
| |
[multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
|
| | |
|
| |
|
|
| |
[tryif t then t2 else t3] behaves like [t;t2] if [t] has at least one success, or [t3] otherwise. It generalises [t||t3] as failures from [t2] will not be caught.
|
| |
|
|
| |
You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
|
| |
|
|
| |
Documentation also updated.
|
Pierre-Marie Pédrot
Guillaume Melquiond
Enrico Tassi
Matthieu Sozeau
Maxime Dénès
Hugo Herbelin
Lionel Rieg
Pierre Boutillier
Clément Pit--Claudel
Pierre Courtieu
Arnaud Spiwack