Mercurial > cpdt > repo

diff src/MoreDep.v @ 375:d1276004eec9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish pass over LogicProg; change [crush] to take advantage of new [Hint Rewrite] syntax that uses database [core] by default
author Adam Chlipala <adam@chlipala.net>
date Mon, 26 Mar 2012 16:55:59 -0400
parents f7c2bf7f1324
children 31fa03bc0f18
line wrap: on
line diff
--- a/src/MoreDep.v	Mon Mar 26 16:24:19 2012 -0400
+++ b/src/MoreDep.v	Mon Mar 26 16:55:59 2012 -0400
@@ -860,7 +860,7 @@
   induction s; substring.
 Qed.
 
-Hint Rewrite substring_all substring_none : cpdt.
+Hint Rewrite substring_all substring_none.
 
 Lemma substring_split : forall s m,
   substring 0 m s ++ substring m (length s - m) s = s.
@@ -883,12 +883,12 @@
 Lemma substring_app_snd : forall s2 s1 n,
   length s1 = n
   -> substring n (length (s1 ++ s2) - n) (s1 ++ s2) = s2.
-  Hint Rewrite <- minus_n_O : cpdt.
+  Hint Rewrite <- minus_n_O.
 
   induction s1; crush.
 Qed.
 
-Hint Rewrite substring_app_fst substring_app_snd using solve [trivial] : cpdt.
+Hint Rewrite substring_app_fst substring_app_snd using solve [trivial].
 (* end hide *)
 
 (** A few auxiliary functions help us in our final matcher definition.  The function [split] will be used to implement the regexp concatenation case. *)
@@ -946,7 +946,7 @@
   induction s; crush.
 Qed.
 
-Hint Rewrite app_empty_end : cpdt.
+Hint Rewrite app_empty_end.
 
 Lemma substring_self : forall s n,
   n <= 0
@@ -960,12 +960,12 @@
   induction s; substring.
 Qed.
 
-Hint Rewrite substring_self substring_empty using omega : cpdt.
+Hint Rewrite substring_self substring_empty using omega.
 
 Lemma substring_split' : forall s n m,
   substring n m s ++ substring (n + m) (length s - (n + m)) s
   = substring n (length s - n) s.
-  Hint Rewrite substring_split : cpdt.
+  Hint Rewrite substring_split.
 
   induction s; substring.
 Qed.
@@ -1020,7 +1020,7 @@
 Qed.
 
 Hint Rewrite substring_stack substring_stack' substring_suffix
-  using omega : cpdt.
+  using omega.
 
 Lemma minus_minus : forall n m1 m2,
   m1 + m2 <= n
@@ -1032,7 +1032,7 @@
   intros; omega.
 Qed.
 
-Hint Rewrite minus_minus using omega : cpdt.
+Hint Rewrite minus_minus using omega.
 (* end hide *)
 
 (** One more helper function will come in handy: [dec_star], for implementing another linear search through ways of splitting a string, this time for implementing the Kleene star. *)
@@ -1098,7 +1098,7 @@
     \/ exists l, l < length s - n
       /\ P (substring n (S l) s)
       /\ star P (substring (n + S l) (length s - (n + S l)) s).
-    Hint Rewrite plus_n_Sm' : cpdt.
+    Hint Rewrite plus_n_Sm'.
 
     intros;
       match goal with