let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
CicPp.pp t names
;;
+
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 applicative_case dbd
tables depth subst fake_proof goalno goalty metasenv context
- universe cache flags
+ signature universe cache flags
=
- let goalty_aux =
+ (* let goalty_aux =
match goalty with
| Cic.Appl (hd::tl) ->
Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
| _ -> goalty
- in
+ in *)
+ let goalty_aux = goalty in
let candidates =
get_candidates flags.skip_trie_filtering universe cache goalty_aux
in
+ (* 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
let tables, elems =
List.fold_left
(fun (tables,elems) cand ->
(lazy ("smart_candidates" ^ " = " ^
(String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
debug_print debug_msg;
-(* we only filter the smart candidates since they could be too many *)
let candidates = List.filter (only signature context metasenv) candidates in
let smart_candidates =
List.filter (only signature context metasenv) smart_candidates
else
applicative_case dbd
tables depth s fake_proof goalno
- gty m context universe cache flags
+ gty m context signature universe cache flags
in
elems@more_elems, tables, cache, flags
else
gty m context signature universe cache flags
| None ->
applicative_case dbd tables depth s fake_proof goalno
- gty m context universe cache flags
+ gty m context signature universe cache flags
in
elems, tables, cache, flags
;;