let module C2A = Cic2acic in
(* atomic terms are never lifted, according to my policy *)
function
- C.ARel (id,_,_,_) -> false
+ C.ARel (id,_,_,_) ->
+ (try
+ ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
+ true;
+ with Not_found -> false)
| C.AVar (id,_,_) ->
(try
ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
K.proof_conclude =
{ K.conclude_id = gen_id conclude_prefix seed;
K.conclude_aref = id;
- K.conclude_method = "Rewrite";
+ K.conclude_method =
+ if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI then
+ "RewriteLR"
+ else
+ "RewriteRL";
K.conclude_args =
K.Term (false,(C.AConst (sid,uri,exp_named_subst)))::method_args;
K.conclude_conclusion =