added syntax for URIs

[helm.git] / helm / ocaml / cic_transformations / ast2pres.ml

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 87944aa34f23a98028573c59c3a445fef78ae1c5..0eba3757fcb5b016846151d19b63ec9742177878 100644 (file)
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -77,8 +77,10 @@ and countterm current_size t =
                let size1 = countvar c var in
                countterm size1 s) current_size l in
           countterm size1 t
-    | A.Ident(s,None) -> current_size + (String.length s)
-    | A.Ident(s,Some l) ->
+    | A.Ident (s,None)
+    | A.Uri (s, None) -> current_size + (String.length s)
+    | A.Ident (s,Some l)
+    | A.Uri (s,Some l) ->
         List.fold_left 
           (fun c (v,t) -> countterm (c + (String.length v)) t) 
           (current_size + (String.length s)) l
@@ -278,7 +280,8 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
           make_defs "let rec" vars in
         Box.V(make_attributes [Some "helm","xref"] [xref],
               definitions@[ast2box ~tail body])
-    | A.Ident (s, subst) ->
+    | A.Ident (s, subst)
+    | A.Uri (s, subst) ->
         let subst =
           let rec make_substs start_txt = 
             function
@@ -423,7 +426,8 @@ let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) =
     | A.Symbol (name,_) -> 
         let attr = make_std_attributes xref in
         P.Mi (attr,name)
-    | A.Ident (name,subst) ->
+    | A.Ident (name,subst)
+    | A.Uri (name,subst) ->
         let attr = make_std_attributes xref in
         let rec make_subst =
           (function