X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fring.ml;h=82ef5f4f2b239a3cfed99092230632e180e51709;hb=04dc7b17e463fa9c75ac91e1df88bf37ed009914;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..82ef5f4f2 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, _subst, _, _, _) = proof in
     let (_, context, _) = CicUtil.lookup_meta goal metasenv in
      let proof',goal' = aux count context status in
       assert (goal = goal') ;
@@ -486,10 +486,10 @@ let ring_tac status =
 	ProofEngineTypes.apply_tactic 
          (Tacticals.first
           ~tactics:[
-            "reflexivity", EqualityTactics.reflexivity_tac ;
-            "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
-            "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ;
-            "exact sym_eqt su t1 ...", exact_tac
+            EqualityTactics.reflexivity_tac ;
+            exact_tac ~term:t1'_eq_t1'' ;
+            exact_tac ~term:t2'_eq_t2'' ;
+            exact_tac
             ~term:(
               Cic.Appl
                [mkConst HelmLibraryObjects.Logic.sym_eq_URI
@@ -499,11 +499,11 @@ let ring_tac status =
                  ] ;
                 t1'_eq_t1''
                ]) ;
-            "elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status ->
+            ProofEngineTypes.mk_tactic (fun status ->
               let status' = (* status after 1st elim_type use *)
                 let context = context_of_status status in
 		let b,_ = (*TASSI : FIXME*)
-		  are_convertible context t1'' t1 CicUniv.empty_ugraph in 
+		  are_convertible context t1'' t1 CicUniv.oblivion_ugraph in 
                 if not b then begin
                   warn (lazy "t1'' and t1 are NOT CONVERTIBLE");
                   let newstatus =
@@ -529,9 +529,8 @@ let ring_tac status =
 	       ProofEngineTypes.apply_tactic
                 (Tacticals.first (* try to solve 1st subgoal *)
                   ~tactics:[
-                    "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
-                    "exact sym_eqt su t2 ...",
-                      exact_tac
+                    exact_tac ~term:t2'_eq_t2'';
+                    exact_tac
                        ~term:(
                          Cic.Appl
                           [mkConst HelmLibraryObjects.Logic.sym_eq_URI
@@ -541,12 +540,12 @@ let ring_tac status =
                             ] ;
                            t2'_eq_t2''
                           ]) ;
-                    "elim_type eqt su t2 ...", 
 		     ProofEngineTypes.mk_tactic (fun status ->
                       let status' =
                         let context = context_of_status status in
 			let b,_ = (* TASSI:FIXME *)
-			  are_convertible context t2'' t2 CicUniv.empty_ugraph 
+			  are_convertible context t2'' t2
+                          CicUniv.oblivion_ugraph 
 			in
 			  if not b then begin 
                           warn (lazy "t2'' and t2 are NOT CONVERTIBLE");