...

[helm.git] / components / acic_content / acic2content.ml

diff --git a/components/acic_content/acic2content.ml b/components/acic_content/acic2content.ml
index b61cb1225e0cf4e9c997657ee9b4f7e87a210fba..69a1f632dcf3117138c5b421dcfb94f9999adb10 100644 (file)
--- a/components/acic_content/acic2content.ml
+++ b/components/acic_content/acic2content.ml
@@ -360,7 +360,7 @@ let infer_dependent ~headless context metasenv = function
                   (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
@@ -942,7 +942,8 @@ and rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_s
               { 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";