X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationUtil.ml;h=7eccd79017d309044abe9e35f17355b4d01872b4;hb=b367de0252e88d6b0476648d5ceac7e4aeffca27;hp=b426863cf613e7f77d1123bb89cf747fe4ac18cf;hpb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml
index b426863cf..7eccd7901 100644
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -63,7 +63,8 @@ let visit_ast ?(special_k = fun _ -> assert false)
       | Ast.Variable _) as t -> special_k t
     | (Ast.Ident _
       | Ast.NRef _
-      | Ast.Implicit
+      | Ast.NCic _
+      | Ast.Implicit _
       | Ast.Num _
       | Ast.Sort _
       | Ast.Symbol _
@@ -208,7 +209,7 @@ let meta_names_of_term term =
     | Ast.Ident (_, Some substs) -> aux_substs substs
     | Ast.Meta (_, substs) -> aux_meta_substs substs
 
-    | Ast.Implicit
+    | Ast.Implicit _
     | Ast.Ident _
     | Ast.Num _
     | Ast.Sort _
@@ -406,11 +407,11 @@ let freshen_obj obj =
           indtypes
       in
       CicNotationPt.Inductive (freshen_capture_variables params, indtypes)
-  | CicNotationPt.Theorem (flav, n, t, ty_opt) ->
+  | CicNotationPt.Theorem (flav, n, t, ty_opt,p) ->
       let ty_opt =
         match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
       in
-      CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt)
+      CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt,p)
   | CicNotationPt.Record (params, n, ty, fields) ->
       CicNotationPt.Record (freshen_capture_variables params, n,
         freshen_term ty, freshen_name_ty_b fields)