bugfix: Ring will work again with varmaps :-)

diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml
index 080e280b5f25325f1faf2daaa141ad8b2e3f5414..c9e50be29a59792060563860f077534d71b7e170 100644 (file)
--- 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))
 
   (**