X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fring.ml;h=0bc26514d45819ce8e4e2e026edf50c7f765519f;hb=0978a9c19e672bb0b505f25737078409381700c7;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..0bc26514d 100644
--- a/helm/software/components/tactics/ring.ml
+++ b/helm/software/components/tactics/ring.ml
@@ -122,14 +122,14 @@ let cic_is_const ?(uri: uri option = None) term =
     @param proof a proof
     @return the uri of a given proof
   *)
-let uri_of_proof ~proof:(uri, _, _, _) = uri
+let uri_of_proof ~proof:(uri, _, _, _, _) = uri
 
   (**
     @param status current proof engine status
     @raise Failure if proof is None
     @return current goal's metasenv
   *)
-let metasenv_of_status ((_,m,_,_), _) = m
+let metasenv_of_status ((_,m,_,_, _), _) = m
 
   (**
     @param status a proof engine status
@@ -444,10 +444,10 @@ 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
+   let (_, metasenv, _, _, _) = proof in
     let (_, context, _) = CicUtil.lookup_meta goal metasenv in
      let proof',goal' = aux count context status in
       assert (goal = goal') ;