From: Enrico Tassi Date: Mon, 2 Oct 2006 11:29:49 +0000 (+0000) Subject: restored old (r6662) behaviour X-Git-Tag: 0.4.95@7852~963 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8100282b272a35d42aa29a94d6d887e673a7298f;p=helm.git restored old (r6662) behaviour --- 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, _) ->