From 8100282b272a35d42aa29a94d6d887e673a7298f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 2 Oct 2006 11:29:49 +0000 Subject: [PATCH] restored old (r6662) behaviour --- components/cic/discrimination_tree.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/components/cic/discrimination_tree.ml b/components/cic/discrimination_tree.ml index 9d6914847..937188dca 100644 --- a/components/cic/discrimination_tree.ml +++ b/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, _) -> -- 2.39.2