X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=42214b57bc4861f979ddac93f83569e09dbb437c;hb=1f974ca07c502d85c9a3760aaaf633bae3c84fb6;hp=22936c1a4531a6338dcb2ca3e7916cf062f41490;hpb=cea3a50f515d1e39467073d2b447a9ddfa1a4852;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 22936c1a4..42214b57b 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -24,6 +24,7 @@
  *)
 
 module C    = Cic
+module I    = CicInspect
 module D    = Deannotate
 module DTI  = DoubleTypeInference
 module TC   = CicTypeChecker 
@@ -286,13 +287,13 @@ and mk_proof st = function
          let decurry = List.length classes - List.length tl in
          if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else
          if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else
-	 let synth = Cl.S.singleton 0 in
+	 let synth = I.S.singleton 0 in
          let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
          match rc with
             | Some (i, j) when i > 1 && i <= List.length classes ->
 	       let classes, tl, _, what = split2_last classes tl in
 	       let script, what = mk_atomic st dtext what in
-	       let synth = Cl.S.add 1 synth in
+	       let synth = I.S.add 1 synth in
 	       let qs = mk_bkd_proofs (next st) synth classes tl in
                if is_rewrite_right hd then 
 	          List.rev script @ convert st t @
@@ -330,8 +331,8 @@ and mk_bkd_proofs st synth classes ts =
 try 
    let _, dtext = test_depth st in   
    let aux inv v =
-      if Cl.overlaps synth inv then None else
-      if Cl.S.is_empty inv then Some (mk_proof st v) else
+      if I.overlaps synth inv then None else
+      if I.S.is_empty inv then Some (mk_proof st v) else
       Some [T.Apply (v, dtext ^ "dependent")]
    in
    T.list_map2_filter aux classes ts