From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 2 Jul 2002 08:05:52 +0000 (+0000)
Subject: bugfix: Ring will work again with varmaps :-)
X-Git-Tag: V_0_3_0_debian_8~10
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5c7da113f9dc24a24274c8196af72450d40fc618;p=helm.git

bugfix: Ring will work again with varmaps :-)
---

diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml
index 080e280b5..c9e50be29 100644
--- a/helm/gTopLevel/ring.ml
+++ b/helm/gTopLevel/ring.ml
@@ -339,8 +339,11 @@ let abstract_poly ~terms ~proof =
         newvar
       end
   in
-  (List.map aux terms,
-   btree_of_array ~vars:(Array.of_list (List.rev !varlist)) ~proof)
+  let aterms = List.map aux terms in  (* abstract vars *)
+  let varmap =  (* build varmap *)
+    btree_of_array ~vars:(Array.of_list (List.rev !varlist)) ~proof
+  in
+  (aterms, varmap)
 
   (**
     given a list of abstract terms (i.e. apolynomials) build the ring "segments"
@@ -451,6 +454,7 @@ let next_goal ~status =
     @param proof term used to prove second subgoal generated by elim_type
   *)
 let elim_type2_tac ~status ~term ~proof =
+  warn "in Ring.elim_type2";
   exact_tac ~term:proof ~status:(next_goal (elim_type_tac ~term ~status))
 
   (**