1. is_meta_closed should be applied only to terms on which a substitution

[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..937188dcae30ebca3fcec1219201271157a210a1 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,14 +291,18 @@ 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
             | DiscriminationTree.Node (_, map) ->
                 let res =
+                  let hd_term = 
+                    elem_of_cic (head_of_term (subterm_at_pos pos term)) 
+                  in
+                  if hd_term = Variable then A.empty else
                   try
-                    let hd_term = head_of_term (subterm_at_pos pos term) in
-                    let n = PSMap.find (elem_of_cic hd_term) map in
+                    let n = PSMap.find hd_term map in
                       match n with
                         | DiscriminationTree.Node (Some s, _) -> s
                         | DiscriminationTree.Node (None, _) ->
@@ -347,6 +355,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
@@ -365,9 +374,10 @@ let remove_index tree equality =
                           (List.map (fun t -> retrieve t term newpos) jl)
                   | Some subterm ->
                       let res = 
+                        let hd_term = elem_of_cic (head_of_term subterm) in
+                        if hd_term = Variable then A.empty else
                         try
-                          let hd_term = head_of_term subterm in
-                          let n = PSMap.find (elem_of_cic hd_term) map in
+                          let n = PSMap.find hd_term map in
                             match n with
                               | DiscriminationTree.Node (Some s, _) -> s
                               | DiscriminationTree.Node (None, _) ->