Proof size nicely reduced using distributive branching with goal selector.

[helm.git] / components / tactics / declarative.ml

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 26276f97c072a75dba7c3fb967697cb4e347e4a9..c669a4161defd736fde2cdd6d1774b3db095b911 100644 (file)
--- a/components/tactics/declarative.ml
+++ b/components/tactics/declarative.ml
@@ -136,7 +136,7 @@ let andelim = existselim;;
 
 let rewritingstep ~dbd ~universe lhs rhs just last_step =
  let aux ((proof,goal) as status) =
-  let (curi,metasenv,proofbo,proofty) = proof in
+  let (curi,metasenv,proofbo,proofty, attrs) = proof in
   let _,context,gty = CicUtil.lookup_meta goal metasenv in
   let eq,trans =
    match LibraryObjects.eq_URI () with
@@ -196,7 +196,7 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step =
              FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context
                (Cic.Name name) ~typ
            in
-            let proof = curi,metasenv,proofbo,proofty in
+            let proof = curi,metasenv,proofbo,proofty, attrs in
             let proof,goals =
              ProofEngineTypes.apply_tactic
               (Tacticals.thens