let is_propositional context sort =
match CicReduction.whd context sort with
| Cic.Sort Cic.Prop
| Cic.Sort (Cic.CProp _) -> true
| _-> false
;;
let is_propositional context sort =
match CicReduction.whd context sort with
| Cic.Sort Cic.Prop
| Cic.Sort (Cic.CProp _) -> true
| _-> false
;;
let is_in_prop context subst metasenv ty =
let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
is_propositional context sort
let is_in_prop context subst metasenv ty =
let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
is_propositional context sort
with
| None, active, passive, bag ->
raise (ProofEngineTypes.Fail (lazy ("paramod fails")))
with
| None, active, passive, bag ->
raise (ProofEngineTypes.Fail (lazy ("paramod fails")))
+ (* if the goal is an equality we skip the congruence theorems
+ let candidates =
+ if is_equational_case goalty flags
+ then List.filter not_default_eq_term candidates
+ else candidates
+ in *)
+ let candidates = List.filter (only signature context metasenv) candidates
+ in
(lazy ("smart_candidates" ^ " = " ^
(String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
debug_print debug_msg;
(lazy ("smart_candidates" ^ " = " ^
(String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
debug_print debug_msg;
let candidates = List.filter (only signature context metasenv) candidates in
let smart_candidates =
List.filter (only signature context metasenv) smart_candidates
let candidates = List.filter (only signature context metasenv) candidates in
let smart_candidates =
List.filter (only signature context metasenv) smart_candidates
in
elems@more_elems, tables, cache, flags
else
in
elems@more_elems, tables, cache, flags
else
in
elems, tables, cache, flags
;;
in
elems, tables, cache, flags
;;
let _,metasenv,subst,_,_, _ = proof in
let _,context,goalty = CicUtil.lookup_meta goal metasenv in
let signature = MetadataQuery.signature_of metasenv goal in
let _,metasenv,subst,_,_, _ = proof in
let _,context,goalty = CicUtil.lookup_meta goal metasenv in
let signature = MetadataQuery.signature_of metasenv goal in