]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_procedural/proceduralClassify.ml
- Coq/preamble: missing alias added
[helm.git] / helm / software / components / acic_procedural / proceduralClassify.ml
index e69b471ca265400e5057f99c5870529c85072e3f..53c363a428372c447284c5c3f5654dbc2cd69f4b 100644 (file)
@@ -56,6 +56,12 @@ let out_table b =
    Array.iteri map b;
    prerr_newline ()
 
+(* dummy dependences ********************************************************)
+
+let make l =
+   let map _ = I.S.empty, false in
+   List.rev_map map l
+
 (* classification ***********************************************************)
 
 let classify_conclusion vs = 
@@ -78,7 +84,7 @@ let classify_conclusion vs =
  
 let classify c t =
 try   
-   let vs, h = PEH.split_with_normalize (c, t) in
+   let vs, h = PEH.split_with_whd (c, t) in
    let rc = classify_conclusion vs in
    let map (b, h) (c, v) = 
       let _, argsno = PEH.split_with_whd (c, v) in