- name mangling changed, added __ to separate additional number

[helm.git] / helm / software / components / tactics / ring.ml

diff --git a/helm/software/components/tactics/ring.ml b/helm/software/components/tactics/ring.ml
index b2d3032706960ca8757588c695cdd16741f48ed2..82ef5f4f2b239a3cfed99092230632e180e51709 100644 (file)
--- 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
@@ -447,7 +447,7 @@ let purge_hyps_tac ~count =
           (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') ;
@@ -503,7 +503,7 @@ let ring_tac 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 =
@@ -544,7 +544,8 @@ let ring_tac 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");