X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fring.ml;h=4d05ab3333cafba2b10fddfa9b383c7450602d39;hb=9fa0f092e8c7500a3890a73893483b44c56db171;hp=4c58f1004ff86e63c014437e41fb50d18a5520cb;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/tactics/ring.ml b/helm/software/components/tactics/ring.ml
index 4c58f1004..4d05ab333 100644
--- a/helm/software/components/tactics/ring.ml
+++ b/helm/software/components/tactics/ring.ml
@@ -444,7 +444,7 @@ let purge_hyps_tac ~count =
         in
          aux (n-1) tl
           (status_of_single_goal_tactic_result 
-	   (ProofEngineTypes.apply_tactic (S.clear ~hyp:name_of_hyp) status))
+	   (ProofEngineTypes.apply_tactic (S.clear ~hyps:[name_of_hyp]) status))
     | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
   in
    let (_, metasenv, _, _) = proof in