Mercurial > cpdt > repo

diff src/Large.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 4550dedad73a
children d5112c099fbf
line wrap: on
line diff
--- a/src/Large.v	Mon Mar 26 16:24:19 2012 -0400
+++ b/src/Large.v	Mon Mar 26 16:55:59 2012 -0400
@@ -208,7 +208,7 @@
 
 Reset eval_times.
 
-Hint Rewrite mult_plus_distr_l : cpdt.
+Hint Rewrite mult_plus_distr_l.
 
 Theorem eval_times : forall k e,
   eval (times k e) = k * eval e.
@@ -421,7 +421,7 @@
   crush.
 Qed.
 
-Hint Rewrite confounder : cpdt.
+Hint Rewrite confounder.
 
 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
 (* begin thide *)
@@ -468,19 +468,19 @@
   Undo.
   info t.
   (** %\vspace{-.15in}%[[
- == simpl in *; intuition; subst; autorewrite with cpdt in *; 
-    simpl in *; intuition; subst; autorewrite with cpdt in *; 
+ == simpl in *; intuition; subst; autorewrite with core in *; 
+    simpl in *; intuition; subst; autorewrite with core in *; 
     simpl in *; intuition; subst; destruct (reassoc e2).
     simpl in *; intuition.
     
     simpl in *; intuition.
     
-    simpl in *; intuition; subst; autorewrite with cpdt in *;
+    simpl in *; intuition; subst; autorewrite with core in *;
        refine (eq_ind_r
                  (fun n : nat =>
                   n * (eval e3 + 1 - 1) * eval e4 = eval e1 * eval e2) _ IHe1);
-       autorewrite with cpdt in *; simpl in *; intuition; 
-    subst; autorewrite with cpdt in *; simpl in *; 
+       autorewrite with core in *; simpl in *; intuition; 
+    subst; autorewrite with core in *; simpl in *; 
     intuition; subst.
  
     ]]
@@ -491,15 +491,15 @@
 
   (** We arbitrarily split the script into chunks.  The first few seem not to do any harm. *)
 
-  simpl in *; intuition; subst; autorewrite with cpdt in *.
-  simpl in *; intuition; subst; autorewrite with cpdt in *.
+  simpl in *; intuition; subst; autorewrite with core in *.
+  simpl in *; intuition; subst; autorewrite with core in *.
   simpl in *; intuition; subst; destruct (reassoc e2).
   simpl in *; intuition.
   simpl in *; intuition.
 
   (** The next step is revealed as the culprit, bringing us to the final unproved subgoal. *)
 
-  simpl in *; intuition; subst; autorewrite with cpdt in *.
+  simpl in *; intuition; subst; autorewrite with core in *.
 
   (** We can split the steps further to assign blame. *)
 
@@ -508,13 +508,13 @@
   simpl in *.
   intuition.
   subst.
-  autorewrite with cpdt in *.
+  autorewrite with core in *.
 
   (** It was the final of these four tactics that made the rewrite.  We can find out exactly what happened.  The [info] command presents hierarchical views of proof steps, and we can zoom down to a lower level of detail by applying [info] to one of the steps that appeared in the original trace. *)
 
   Undo.
 
-  info autorewrite with cpdt in *.
+  info autorewrite with core in *.
   (** %\vspace{-.15in}%[[
  == refine (eq_ind_r (fun n : nat => n = eval e1 * eval e2) _
               (confounder (reassoc e1) e3 e4)).