From bd6fc1fca8a907b950893a9af81ed1a79903c887 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 22 Feb 2011 22:12:53 +0000 Subject: 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 --- test-suite/success/Hints.v | 2 -- 1 file changed, 2 deletions(-) (limited to 'test-suite/success') 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. -- cgit v1.2.3