weight of non oriented equations decreased
+let rec remove_local_context =
+ function
+ | Cic.Meta (i,_) -> Cic.Meta (i,[])
+ | Cic.Appl l ->
+ Cic.Appl(List.map remove_local_context l)
+ | t -> t
+
(************************* rpo ********************************)
let number = [
(************************* rpo ********************************)
let number = [
~consider_metas:true ~count_metas_occurrences:false right) in
let w2, m2 = (weight_of_term
~consider_metas:true ~count_metas_occurrences:false left) in
~consider_metas:true ~count_metas_occurrences:false right) in
let w2, m2 = (weight_of_term
~consider_metas:true ~count_metas_occurrences:false left) in
- w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
+ (max w1 w2)+(max (factor * (List.length m1)) (factor * (List.length m2)))
val debug_print: string Lazy.t -> unit
val metas_of_term: Cic.term -> int list
val debug_print: string Lazy.t -> unit
val metas_of_term: Cic.term -> int list
+
+val remove_local_context: Cic.term -> Cic.term