RELATIONAL: new undecomposable definition of NLE

[helm.git] / helm / software / components / acic_procedural / acic2Procedural.ml

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 22936c1a4531a6338dcb2ca3e7916cf062f41490..42214b57bc4861f979ddac93f83569e09dbb437c 100644 (file)
--- 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