X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Facic2Ast.ml;h=1bc76ebb841176b185fde2c0052e2168b7130d0a;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;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..1bc76ebb8 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
@@ -78,7 +78,7 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
     | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, astcontext_of_ciccontext l))
     | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
     | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
-    | Cic.ASort (id,Cic.Type) -> idref id (Ast.Sort `Type)
+    | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type) (* TASSI *)
     | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
     | Cic.AImplicit _ -> assert false
     | Cic.AProd (id,n,s,t) ->
@@ -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