restored old (r6662) behaviour

diff --git a/helm/software/components/cic/discrimination_tree.ml b/helm/software/components/cic/discrimination_tree.ml
index 9d691484701477b94554a3d72b4853741ec739f5..937188dcae30ebca3fcec1219201271157a210a1 100644 (file)
--- a/helm/software/components/cic/discrimination_tree.ml
+++ b/helm/software/components/cic/discrimination_tree.ml
@@ -297,9 +297,12 @@ let remove_index tree equality =
             | 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, _) ->
@@ -371,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, _) ->