restored the good factorization file

[helm.git] / helm / software / components / cic / discrimination_tree.ml

diff --git a/helm/software/components/cic/discrimination_tree.ml b/helm/software/components/cic/discrimination_tree.ml
index 33ecea7cecabc2c6bbf93bb0732bd93f8cf91c79..9d691484701477b94554a3d72b4853741ec739f5 100644 (file)
--- a/helm/software/components/cic/discrimination_tree.ml
+++ b/helm/software/components/cic/discrimination_tree.ml
@@ -242,6 +242,10 @@ let remove_index tree equality =
         | term -> term
       ;;
 
+      let rec skip_prods = function
+        | Cic.Prod (_,_,t) -> skip_prods t
+        | term -> term
+      ;;
 
       let rec subterm_at_pos pos term =
         match pos with
@@ -287,6 +291,7 @@ let remove_index tree equality =
       ;;     
 
       let retrieve_generalizations (tree,arity) term =
+        let term = skip_prods term in
         let rec retrieve tree term pos =
           match tree with
             | DiscriminationTree.Node (Some s, _) when pos = [] -> s
@@ -347,6 +352,7 @@ let remove_index tree equality =
 
 
       let retrieve_unifiables (tree,arities) term =
+        let term = skip_prods term in
         let rec retrieve tree term pos =
           match tree with
             | DiscriminationTree.Node (Some s, _) when pos = [] -> s