X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationUtil.ml;h=7eccd79017d309044abe9e35f17355b4d01872b4;hb=5c92c318030a05c766b3f6070dbd23589cbdee04;hp=4e5917a154aa87abdd493d46921e0c8bd07eccf0;hpb=d34061fd1c820139fad38c39dee6377e5057bf26;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml
index 4e5917a15..7eccd7901 100644
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -63,6 +63,7 @@ let visit_ast ?(special_k = fun _ -> assert false)
       | Ast.Variable _) as t -> special_k t
     | (Ast.Ident _
       | Ast.NRef _
+      | Ast.NCic _
       | Ast.Implicit _
       | 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)