]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/tactics/ring.ml
fixed defaultauto behaviour. not the cache is preserveed
[helm.git] / helm / software / components / tactics / ring.ml
index 4c58f1004ff86e63c014437e41fb50d18a5520cb..4d05ab3333cafba2b10fddfa9b383c7450602d39 100644 (file)
@@ -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