X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fring.ml;fp=helm%2Focaml%2Ftactics%2Fring.ml;h=ab7bde56f8dfa4049ca0989ccb55e64d3ac7eada;hb=df0606d3bcbc41272fcde2d013bbe0b1aadf98af;hp=cebb4cf91b35416d73a637cbf73a7aabb5861136;hpb=ded3a0b12793fc8e463a4a3be9f62f54f734897e;p=helm.git

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index cebb4cf91..ab7bde56f 100644
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -437,9 +437,15 @@ let purge_hyps_tac ~count =
     match (n, context) with
     | (0, _) -> status
     | (n, hd::tl) ->
-        aux (n-1) tl
-         (status_of_single_goal_tactic_result 
-	  (ProofEngineTypes.apply_tactic (S.clear ~hyp:hd) status))
+        let name_of_hyp =
+         match hd with
+            None
+          | Some (Cic.Anonymous,_) -> assert false
+          | Some (Cic.Name name,_) -> name
+        in
+         aux (n-1) tl
+          (status_of_single_goal_tactic_result 
+	   (ProofEngineTypes.apply_tactic (S.clear ~hyp:name_of_hyp) status))
     | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
   in
    let (_, metasenv, _, _) = proof in