| 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
;;
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, _) ->
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
(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, _) ->