Imported Upstream version 0.2.pl2upstream/0.2.pl2

1 files changed, 8 insertions, 11 deletions

diff --git a/Caveats.v b/Caveats.v
index 8cef602..0d0d5ca 100644
--- a/Caveats.v
+++ b/Caveats.v
@@ -335,7 +335,8 @@ Goal a+b*c = c.
      *)
 Abort.
 
-(** **** If the pattern is a unit:
+(** **** If the pattern is a unit or can be instanciated to be equal
+   to a unit:
   
    The heuristic is to make the unit appear at each possible position
    in the term, e.g. transforming [a] into [1*a] and [a*1], but this
@@ -351,23 +352,19 @@ Goal a+b+c = c.
   (** 7 solutions, we miss solutions like [(a+b+c+0*(1+0*[]))]*)
 Abort.
 
-(** **** If the pattern is a nullifiable, but not a unit:
-
-   The heuristic is to make units appear around subterms that are
-built with AC or A symbols. Note that this case is relevant only if
-one uses [aacu_rewrite]. *)
-
-Hypothesis H : forall x y, (x+y)*x = x*x + y*x.
+(** *** Another example of the former case is the following, where the hypothesis can be instanciated to be equal to [1] *)
+Hypothesis H : forall x y, (x+y)*x = x*x + y *x.
 Goal a*a+b*a + c = c.
   (** Here, only one solution if we use the aac_instance tactic  *)
   aac_instances <- H.
 
-  (** There are three solutions using aacu_instances (but, here,
+  (** There are 8 solutions using aacu_instances (but, here,
      there are infinitely many different solutions). We miss e.g. [a*a +b*a
      + (x*x + y*x)*c], which seems to be more peculiar. *)
-  aacu_instances <- H. 
-Abort.
+  aacu_instances <- H.
 
+  (** The 7 last solutions are the same as if we were matching [1] *)
+  aacu_instances H1.  Abort.
 
 (** The behavior of the tactic is not satisfying in this case. It is
 still unclear how to handle properly this kind of situation : we plan