| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |\
| |
| |
| | |
Was PR#192: Add test suite files for 4700-4785
|
| | |
| |
| |
| |
| |
| |
| |
| | |
I didn't add any test-cases for timing-based bugs (4707, 4768, 4776,
4777, 4779, 4783), nor CoqIDE bugs (4700, 4751, 4752, 4756), nor
bugs about printing (4709, 4711, 4720, 4723, 4734, 4736, 4738, 4741,
4743, 4748, 4749, 4750, 4757, 4758, 4765, 4784). I'm not sure what to
do with 4712, 4714, 4732, 4740.
|
| | |
| |
| |
| |
| |
| |
| | |
Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations
no longer modify the parser in non-compat-mode, so we can do this
without breaking Ltac parsing. Also update the related test-suite
files.
|
| | |
| |
| |
| |
| | |
It seems warnings are not taken into account in output/
tests.
|
| | | |
|
| | | |
|
| |\ \
| |/
|/| |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
With this commit, it is possible to write notations so that singleton
lists are usable in both 8.4 and 8.5pl1 -compat. Longer lists await the
ability to remove notations from the parser.
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
This gets rid of brittle code written in ML files through Ltac quotations, and
reduces the dependance of Coq to such a feature. This also fixes the particular
instance of bug #2800, although the underlying issue is still there.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
evars were created making in turn that evars formerly recognized as
pending were not anymore in the list of pending evars). This also
fixes the reopening of #3848.
See comments on #4484 for details.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This commit has deep consequences in term of tactic evaluation,
as it allows to pass any tac_arg to ML and alias tactics rather than
mere generic arguments. This makes the evaluation much more uniform,
and in particular it removes the special evaluation function for notations.
This last point may break some notations out there unluckily.
I had to treat in an ad-hoc way the tactic(...) entry of tactic notations
because it is actually not interpreted as a generic argument but rather
as a proper tactic expression instead.
There is for now no syntax to pass any tactic argument to a given ML or
notation tactic, but this should come soon.
Also fixes bug #3849 en passant.
|
| |\| |
|
| |\| |
|
| | | |
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
It breaks test-suite of trunk since Matthieu's fixes for the soundness of
polymorphic universes, and I am unsure of the expected semantics. We should
reintroduce it later on when we understand better the issue of simply fix it
once and for all.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| | |
test-suite.
|
| | |
| |
| |
| |
| |
| | |
Pretype_errors.PretypeError.
Instad of trying to print the exception, we raise it in the tactic monad.
|
| |\|
| |
| |
| |
| |
| |
| | |
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
preserving compatibility of subst after #4214 being solved.
|
| |\| |
|
| | |
| |
| |
| |
| | |
Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.
As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- no more inconsistent Axiom in the Prelude
- STM can now process Admitted proofs asynchronously
- the quick chain can stock "Admitted" jobs in .vio files
- the vio2vo step checks the jobs but does not stock the result
in the opaque tables (they have no slot)
- Admitted emits a warning if the proof is complete
- Admitted uses the (partial) proof term to infer section variables
used (if not given with Proof using), like for Qed
- test-suite: extra line Require TestSuite.admit to each file making
use of admit
- test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to
find TestSuite.admit
|
| | | |
|
| |\| |
|
| | | |
|
Paul Steckler
Maxime Dénès
Jason Gross
Enrico Tassi
Pierre-Marie Pédrot
Hugo Herbelin
Matthieu Sozeau
Matthieu Sozeau
Arnaud Spiwack