(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
{ 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";