X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=bbe76859f3daf7f1ffffaba61175940114e47f85;hb=db235934efa41a0f38e79747f6db4f468367410b;hp=2055bb9cdbe3c2a99c7ef25e4722bafbee87dd6e;hpb=341c09ae53c5b432015dbd95ac099d824609e626;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 2055bb9cd..bbe76859f 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -210,7 +210,7 @@ let cic2grafite context menv t =
       | Cic.Const _ as t -> 
           PT.Ident (pp_t c t, None)
       | Cic.Appl l -> PT.Appl (List.map (aux c) l)
-      | Cic.Implicit _ -> PT.Implicit
+      | Cic.Implicit _ -> PT.Implicit `JustOne
       | Cic.Lambda (Cic.Name n, s, t) ->
           PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
             aux (Some (Cic.Name n, Cic.Decl s)::c) t)
@@ -220,7 +220,7 @@ let cic2grafite context menv t =
       | Cic.LetIn (Cic.Name n, s, ty, t) ->
           PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
             aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t)
-      | Cic.Meta _ -> PT.Implicit
+      | Cic.Meta _ -> PT.Implicit `JustOne
       | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
       | Cic.Sort Cic.Set -> PT.Sort `Set
       | Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)