let premise_prefix = "prem:";;
let lemma_prefix = "lemma:";;
+let hide_coercions = ref true;;
+
(* e se mettessi la conversione di BY nell'apply_context ? *)
(* sarebbe carino avere l'invariante che la proof2pres
generasse sempre prove con contesto vuoto *)
generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
else raise Not_a_proof
| C.AAppl (id,li) ->
- (try rewrite
+ (try coercion
+ seed li ~ids_to_inner_types ~ids_to_inner_sorts
+ with NotApplicable ->
+ try rewrite
seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
try inductive
seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
- try transitivity
+ try transitivity
seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
let subproofs, args =
}
| _ -> raise NotApplicable
+and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts =
+ match li with
+ | ((Cic.AConst _) as he)::tl
+ | ((Cic.AMutInd _) as he)::tl
+ | ((Cic.AMutConstruct _) as he)::tl when
+ CoercDb.is_a_coercion' (Deannotate.deannotate_term he) &&
+ !hide_coercions ->
+ let rec last =
+ function
+ [] -> assert false
+ | [t] -> t
+ | _::tl -> last tl
+ in
+ acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
+ | _ -> raise NotApplicable
+
and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
let module C2A = Cic2acic in