try
let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
if is_a_fact status (mk_cic_term ctx ty) then
try
let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
if is_a_fact status (mk_cic_term ctx ty) then
NCicParamod.forward_infer_step status metasenv subst ctx eq_cache t ty)
else
(noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv ty)));
NCicParamod.forward_infer_step status metasenv subst ctx eq_cache t ty)
else
(noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv ty)));
let universe = status#auto_cache in
let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of gty in
let universe = status#auto_cache in
let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of gty in
let candidates_facts,candidates_other =
let gl1,gl2 = List.partition test global_cands in
let ll1,ll2 = List.partition test local_cands in
let candidates_facts,candidates_other =
let gl1,gl2 = List.partition test global_cands in
let ll1,ll2 = List.partition test local_cands in
- (* if the goal is an equation we avoid to apply unit equalities,
- since superposition should take care of them; refl is an
+ (* if the goal is an equation and paramodulation did not fail
+ we avoid to apply unit equalities; refl is an
app_counter:= !app_counter+1;
let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of gty in
app_counter:= !app_counter+1;
let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of gty in
(* new *)
let candidates_facts, smart_candidates_facts,
candidates_other, smart_candidates_other =
(* new *)
let candidates_facts, smart_candidates_facts,
candidates_other, smart_candidates_other =
let do_something signature flags status g depth gty cache =
(* if the goal is meta we close it with I:True. This should work
let do_something signature flags status g depth gty cache =
(* if the goal is meta we close it with I:True. This should work
if is_meta status gty then
let t = Ast.Ident("I",None) in
debug_print (lazy ("using default term" ^ (NotationPp.pp_term status) t));
if is_meta status gty then
let t = Ast.Ident("I",None) in
debug_print (lazy ("using default term" ^ (NotationPp.pp_term status) t));