(n <> Cic.Anonymous && fstorder src, t) ::
aux (CicSubstitution.subst
(Deannotate.deannotate_term t) tgt) tl
- | _ -> assert false
+ | _ -> List.map (fun s -> false,s) (t::tl)
in
(false, he) :: aux hety tl
with CicTypeChecker.TypeCheckerFailure _ -> assert false
let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_to_inner_types ~ids_to_inner_sorts =
let module C = Cic in
let module K = Content in
- let rec aux =
+ let rec aux n =
function
[] -> [],[]
| (dep, t)::l1 ->
- let subproofs,args = aux l1 in
- if (test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts) then
+ let need_lifting =
+ test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts in
+ let subproofs,args = aux (n + if need_lifting then 1 else 0) l1 in
+ if need_lifting then
let new_subproof =
acic2content
seed context metasenv
- ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in
+ ~name:("H" ^ string_of_int n) ~ids_to_inner_types
+ ~ids_to_inner_sorts t in
let new_arg =
K.Premise
{ K.premise_id = gen_id premise_prefix seed;
| _ -> (K.Term (dep,t))) in
subproofs,hd::args
in
- match (aux (infer_dependent ~headless context metasenv l)) with
+ match (aux 1 (infer_dependent ~headless context metasenv l)) with
[p],args ->
[{p with K.proof_name = None}],
List.map
{ K.conclude_id = gen_id conclude_prefix seed;
K.conclude_aref = id;
K.conclude_method =
- if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI then
+ if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI
+ || LibraryObjects.is_eq_ind_URI uri then
"RewriteLR"
else
"RewriteRL";