added default for matita.noiinertypes

[helm.git] / components / acic_procedural / proceduralClassify.ml

diff --git a/components/acic_procedural/proceduralClassify.ml b/components/acic_procedural/proceduralClassify.ml
index 755176e5c50cc4d4d280fcee4b373089ebbcb485..4c0014d2e320e4e214aa511f66f1694ee9b6ac59 100644 (file)
--- a/components/acic_procedural/proceduralClassify.ml
+++ b/components/acic_procedural/proceduralClassify.ml
@@ -78,12 +78,13 @@ let classify_conclusion vs =
  
 let classify c t =
 try   
-   let vs, h = PEH.split_with_whd (c, t) in
+   let vs, h = PEH.split_with_normalize (c, t) in
    let rc = classify_conclusion vs in
    let map (b, h) (c, v) = 
       let _, argsno = PEH.split_with_whd (c, v) in
+      let isf = argsno > 0 || H.is_sort v in
       let iu = H.is_unsafe h (List.hd vs) in
-      (I.get_rels_from_premise h v, I.S.empty, argsno > 0 && iu) :: b, succ h
+      (I.get_rels_from_premise h v, I.S.empty, isf && iu) :: b, succ h
    in
    let l, h = List.fold_left map ([], 0) vs in
    let b = Array.of_list (List.rev l) in