| Commit message (Collapse) | Author | Age |
|
|
|
|
|
| |
ident by Ltac).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14074 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
for adding spaces were not taken into account in notations containing
patterns of the form "{ ident symbol", paradoxically resulting in
adding extra spaces, e.g. when printing the type "{ x | P x }" of
"exist", due to interferences with the heuristic for adding breaking
points in Metasyntax.make_hunk).
Also adapted output of test InitSyntax.v after commit r14018 improved
the printing of "ex P" and "sig P".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14073 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14060 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14018 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
This reverts commit 33434695615806a85cec88452c93ea69ffc0e719.
Conflicts:
kernel/term_typing.ml
test-suite/success/polymorphism.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13998 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
- Add Set Typeclasses Debug/Depth n options for typeclasses eauto.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13989 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13988 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
which did not test what it was supposed to test
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13970 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
- Missing space and bad constr level in "About f"
- Display of arguments missing when used as a pattern notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13966 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13946 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Probably something related with the unicode lambda syntax...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13911 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13910 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13909 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
Note: I'm unsure about some subtyping error case apparently involving
aliases of inductive types (middle of Subtyping.check_inductive); I
bound it to some NotEqualInductiveAliases error, but this has to be
checked.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13885 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
for the domain instead of retrieving the known domain of the initial evar.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13881 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Before this patch, hints such as "Hint Resolve -> a" in success/Hints.v
were erroneously considered "eauto-only". We try to clarify the big
boolean expression via "if", and for the moment we remove
the detection of "nonlinearity" via duplicated_metas : on the example,
some nonlinearity was found for strange reason (beta expansion ?), and
after some discussion with Hugo, it is unclear whether this nonlinearity
stuff is useful at all. The next coqbench might provide some answer
to this question, we'll see
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13850 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
In particular, the Fail meta-command cannot for the moment catch a Syntax Error,
which is raised by Vernac.parse_sentence, before we even now that the line starts
by a Fail...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13847 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13846 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13821 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
instances of the lemma are rewritten at once. Cleanup dead code and put
the problematic cases in the test-suite. Also fix some test-suite
scripts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13813 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13805 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13797 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13786 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
(backport from 8.3)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13781 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
This variant was ignoring its second argument, and didn't exactly
respect its documented specification. This is fixed by removing the
variant altogether.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13746 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
We now keep some type information in the "info" field of constructors
and cases, and compact a match with some default branches (or remove
this match completely) only if this transformation is type-preserving.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13732 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
of "match" is not general enough; if there is a non dependent type
constraint, we also try w/o inversion predicate in the return clause.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13727 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Thanks to Marc Lasson for the analysis of the problem and for the
initial patch.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13679 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13671 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
Local/Global modifiers in interpretation loop so as to support
Local/Global for grammar extension) that made use of
DuringSyntaxChecking error wrapper inappropriately nested with the
DuringCommandInterp error wrapper, what disturbed the error
processors. Good thing, we can now simplify things and completely
remove the DuringSyntaxChecking wrapper.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13667 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Well, hopefully, that belongs to the past: you should now be able
to do the very same queries as before, without typing the [ ].
For instance: SearchAbout plus mult.
This removal of [ ] is optional, the old syntax is still legal:
- for compatibility reasons
- for square bracket lovers
- for those that have "inside" or "outside" as legal identifier
in their development and want to search about them.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13654 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
option of "auto". Works for not too complicated hints (e.g. "@pair _ _ 0").
Would be simpler if make_apply_entry supported lemmas containing evars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13598 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
The test misc/deps-order was failing in non-local mode.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13560 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
typeclass resolution.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13533 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
no undefined variables in the context now).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13532 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
on unsupported unicode character) + forbidding unsupported unicode in
Notation declarations too.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13526 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
This test it not relevant anyway, thanks to eta...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13513 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
The new output makes sense with the new "1 subgoal = 1 evar" paradigm
introduced with by the new proof engine.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13508 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Obviously broken since r13359 (remove native Π)...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13502 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
I have no idea how this test could have ever worked... (ssreflect?
declarative mode?)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13501 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
discharge bug of implicit arguments related to commit 13484 (multiple
implicit arguments sequences patch).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13500 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13495 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
- fixing r13483 (supposed dead code in impargs was actually half-living:
implicit arguments mode should merge with the {...} manually given
implicit arguments but not with the "Implicit Arguments [...]" arguments),
- fixing code of drop_first_implicits in r13484.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13490 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13487 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]".
This should a priori be used with care (it might be a bit disturbing
seeing the same constant used with apparently incompatible signatures).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- use list of non-newline-ended phrases instead of newline-separated
texts because newline-separated texts does not support well being
put in boxes (e.g. ''v 2 (str"a" ++ fnl()) ++ str"b" ++ fnl()''
prints "b" at indentation 2 while to get the expected output, one
would have needed to have the fnl outside the box as in
''v 2 (str"a") ++ fnl() ++ str"b" ++ fnl()''
- also reason over lists of explicitly non-empty lines instead of
checking for "mt" lines to skip
The reason of this is to permit nesting of printing infos.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13482 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Pratical situation: simple eapply foo on a goal ?123, while foo is a
(forall f, exists ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13479 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
This commit fixes a bug that made the system inconsistent with proof
irrelevance (the main idea being that Set = Prop by reflexivity).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13450 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
of an anomaly).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13442 85f007b7-540e-0410-9357-904b9bb8a0f7
|