X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Facic2Ast.ml;h=e51e9c0a401b3d69accb7790a364e6243ab12836;hb=22f61c7bd18cd3652e886f6a765aab63eacac83c;hp=19b6c4b4bf4161ab4546d2f178fe9e13d2c117be;hpb=b029556cbcecb852dfc9cf25801f3dcc0bb762bb;p=helm.git

diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index 19b6c4b4b..e51e9c0a4 100644
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -70,7 +70,7 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
   let module Ast = CicAst in
   let idref id t = Ast.AttributedTerm (`IdRef id, t) in
   let rec aux = function
-    | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, []))
+    | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None))
     | Cic.AVar (id,uri,subst) ->
         register_uri id (UriManager.string_of_uri uri);
         idref id
@@ -181,7 +181,7 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
             | _ -> assert false)
           with Not_found -> assert false
         in
-        idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, [])))
+        idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None)))
     | Cic.ACoFix (id, no, funs) -> 
         let defs = 
           List.map
@@ -195,11 +195,13 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
             | _ -> assert false)
           with Not_found -> assert false
         in
-        idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, [])))
+        idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, None)))
 
   and astsubst_of_cicsubst subst =
-    List.map (fun (uri, annterm) -> (UriManager.name_of_uri uri, aux annterm))
-      subst
+    Some
+      (List.map (fun (uri, annterm) ->
+        (UriManager.name_of_uri uri, aux annterm))
+        subst)
 
   and astcontext_of_ciccontext context =
     List.map