]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_content/termAcicContent.ml
Coercion hiding implemented. Notes:
[helm.git] / helm / software / components / acic_content / termAcicContent.ml
index 0af74d261701e01a0918040451dc5599e61f19b1..81d0ef0a74f12211cb7a8e74ba7fd504fbf5311e 100644 (file)
@@ -154,11 +154,11 @@ let ast_of_acic0 ~output_type term_info acic k =
                      try HExtlib.split_nth (cpos+sats+1) tl with Failure _ -> [],[] 
                    in
                    if rest = [] then
-                     idref aid (List.nth (List.map k tl) cpos)
+                     idref aid (k (List.nth tl cpos))
                    else
                      idref aid (Ast.Appl (List.map k (List.nth tl cpos::rest)))
                  else
-                   idref aid (Ast.Appl (List.map k tl))
+                   idref aid (Ast.Appl (List.map k args))
            else
              idref aid (Ast.Appl (List.map k args)))
     | Cic.AAppl (aid,args) ->