diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-22 22:12:53 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-22 22:12:53 +0000 |
| commit | bd6fc1fca8a907b950893a9af81ed1a79903c887 (patch) | |
| tree | 06c979e71674da71afb98d0cb5c1411725004094 /test-suite | |
| parent | 4a2bd45d6b3c2adc90ac547f5afc0ebdd51c3293 (diff) | |
Try to fix the behavior of clenv_missing used when declaring hints
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
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Hints.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 6bbb0ff17..a93f89000 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -51,8 +51,6 @@ Axiom a : forall n, n=0 <-> n<=0. Hint Resolve -> a. Goal forall n, n=0 -> n<=0. auto. - -Print Hints Qed. |