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 *)
}
in
generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
- else raise Not_a_proof
+ else
+ raise Not_a_proof
| C.ALetIn (id,n,s,t) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
if sort = `Prop then
{ proof' with
K.proof_name = None;
K.proof_context =
- ((build_def_item seed id n s ids_to_inner_sorts
+ ((build_def_item seed (get_id s) n s ids_to_inner_sorts
ids_to_inner_types):> Cic.annterm K.in_proof_context_element)
::proof'.K.proof_context;
}
in
generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
- else raise Not_a_proof
+ 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