| Commit message (Collapse) | Author | Age |
|\ |
|
| |\
| | |
| | |
| | | |
Was PR#293: Fix #4762 (eauto weaker than auto).
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
This is a quick fix. The Metasyntax module should be thoroughly revised
in trunk, because it starts featuring a lot of spaghetti code and redundant
data.
|
| | |
| | |
| | |
| | |
| | | |
It seems warnings are not taken into account in output/
tests.
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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 avoids leakage of universes. Also makes
Program Lemma/Fact work again, it tries to solve the
remaining evars using the obligation tactic.
|
| | |
|
|\ \
| | |
| | |
| | | |
Was PR#232: Fix the parsing of goal selectors.
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
Importing VectorNotations breaks `; []`. So we make sure it's not
imported by defualt. Some files might be required to `Import
VectorDef.VectorNotations` rather than just `Import VectorNotations`.
|
| | |
| | |
| | |
| | |
| | | |
Also delimit vector_scope with vector, so that people can write %vector
without having to delimit it themselves.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The no-inversion and maximal abstraction over dependencies now
supports abstraction over goal variables rather than only on "rel"
variables. In particular, it now works consistently using
"intro H; refine (match H with ... end)" or
"refine (fun H => match H with ... end)".
By doing so, we ensure that all three strategies are tried in all
situations where a return clause has to be inferred, even in the
context of a "refine".
See antepenultimate commit for discussion.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
even when no type constraint is given.
This no-inversion and maximal abstraction over dependencies in (rel)
variables heuristic was used only when a type constraint was given.
By doing so, we ensure that all three strategies "inversion with
dependencies as evars", "no-inversion and maximal abstraction over
dependencies in (rel) variables", "no-inversion and no abstraction
over dependencies" are tried in all situations where a return clause
has to be inferred.
See penultimate commit for discussion.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The no-inversion no-dependency heuristic was used only in the absence
of type constraint. We may now use it also in the presence of a type
constraint.
See previous commit for discussion.
|
| | | |
|
| | | |
|
|\ \ \
| | |/
| |/| |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | | |
Getting closer from before when the bug was introduced + test.
|
|\| | |
|
| | | |
|
| | | |
|
| | | |
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Uses sed 's/\s*[0-9]*\.[0-9]\+\s*//g' and 's/\s*0\.\s*//g' to strip
numbers of seconds and to strip percentages. (This can potentially be
extended later.)
Add a test-suite file to make sure that LtacProf outputs some table.
|
| | | |
| | | |
| | | |
| | | |
| | | | |
This required improving the machinery of the test-suite Makefile to
support -compile.
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Add a boolean for refolding during reduction, and an option
that is off by default in 8.6, to turn refolding on in all reduction
functions, as in 8.5.
|
|/ / / |
|
| | |
| | |
| | |
| | | |
This was making the test-suite fail on machines where csdp was not installed.
|
| | |
| | |
| | |
| | | |
esprit d'escalier : is now also fixed for R
|
| | |
| | |
| | |
| | |
| | | |
The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm)
instead of apply (__arith P1 ... Pn) which unification could fail.
|
|\| | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
- Assert a purely arihtmetic sub-goal that is proved independently by reflexion.
(This reduces the stress on the conversion test)
- Does not use 'abstract' anymore (more natural proof-term)
- Fix a parsing bug (certain terms in Prop where not recognized)
|
| | | |
|
|\| | |
|
| | | |
|
| | |
| | |
| | |
| | | |
If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.
|
| | |
| | |
| | |
| | |
| | |
| | | |
We add a flag Keep Admitted Variables that allows to recover the legacy
v8.4 behaviour of admitted lemmas. The statement of such lemmas did not
depend on the current context variables.
|
| | | |
|
| | | |
|