From 5c7da113f9dc24a24274c8196af72450d40fc618 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 2 Jul 2002 08:05:52 +0000 Subject: [PATCH] bugfix: Ring will work again with varmaps :-) --- helm/gTopLevel/ring.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) 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)) (** -- 2.39.2